| ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x2 x3 ⟶ x1 x3 x2) ⟶ (∀ x2 . x2 ⊆ x0 ⟶ atleastp u3 x2 ⟶ not (∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ x1 x3 x4)) ⟶ ∀ x2 . x2 ⊆ x0 ⟶ equip x2 u4 ⟶ ∀ x3 x4 : ι → ι . (∀ x5 . x5 ∈ u4 ⟶ x3 x5 ∈ x2) ⟶ (∀ x5 . x5 ∈ u4 ⟶ x4 x5 ∈ x2) ⟶ (∀ x5 . x5 ∈ u4 ⟶ x3 x5 = x4 x5 ⟶ ∀ x6 : ο . x6) ⟶ (∀ x5 . x5 ∈ u4 ⟶ x1 (x3 x5) (x4 x5)) ⟶ (∀ x5 . x5 ∈ u4 ⟶ ∀ x6 . x6 ∈ u4 ⟶ x3 x5 = x3 x6 ⟶ x4 x5 = x4 x6 ⟶ x5 = x6) ⟶ (∀ x5 . x5 ∈ u4 ⟶ ∀ x6 . x6 ∈ u4 ⟶ x3 x5 = x4 x6 ⟶ x4 x5 = x3 x6 ⟶ x5 = x6) ⟶ f1360.. x1 u3 x2 |
|