exact ⟨z, _, b, _, ⟨rfl, rfl⟩, hz, hb⟩
case h.mpr.intro.intro
V : Type u_1
inst✝ : Zermelo V
r x y z✝ s : V
h : ran r ⊆ dom s
t b : V
hb : opair t b ∈ r
this : b ∈ ran r
z : V
hz : opair b z ∈ s
⊢ ∃ z a b c, (t = a ∧ z = c) ∧ opair b c ∈ s ∧ opair a b ∈ r
no goals