∀ x0 : ι → ι → ο . (∀ x1 . x1 ⊆ u12 ⟶ atleastp u5 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ⊆ u16 ⟶ atleastp u6 x1 ⟶ (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ not (x0 x2 x3)) ⟶ atleastp u2 (setminus x1 u12) |
|