| ∀ x0 : ι → ι → ο . ∀ x1 x2 x3 . x0 x1 x2 ⟶ x0 x1 x3 ⟶ x0 x2 x3 ⟶ (∀ x4 . x4 ∈ SetAdjoin (UPair x1 x2) x3 ⟶ ∀ x5 . x5 ∈ SetAdjoin (UPair x1 x2) x3 ⟶ x0 x4 x5 ⟶ x0 x5 x4) ⟶ ∀ x4 . x4 ∈ SetAdjoin (UPair x1 x2) x3 ⟶ ∀ x5 . x5 ∈ SetAdjoin (UPair x1 x2) x3 ⟶ (x4 = x5 ⟶ ∀ x6 : ο . x6) ⟶ x0 x4 x5 |
|