constructor
case h
x : ℤ
⊢ x ∈ {x | |3 * x| < 24} ↔ x ∈ {-7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
case h.mp
x : ℤ
⊢ x ∈ {x | |3 * x| < 24} → x ∈ {-7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}

case h.mpr
x : ℤ
⊢ x ∈ {-7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7} → x ∈ {x | |3 * x| < 24}