intro t ht
case inr
V : Type u_1
inst✝ : Zermelo V
x y a : V
ha : a ∈ x
b : V
hb : b ∈ y
⊢ pair a b ⊆ x ∪ y
case inr
V : Type u_1
inst✝ : Zermelo V
x y a : V
ha : a ∈ x
b : V
hb : b ∈ y
t : V
ht : t ∈ pair a b
⊢ t ∈ x ∪ y