- oa_leq_refl: ∀a:oa_P. oa_leq a a;
- oa_leq_antisym: ∀a,b:oa_P.oa_leq a b → oa_leq b a → a = b;
- oa_leq_trans: ∀a,b,c:oa_P.oa_leq a b → oa_leq b c → oa_leq a c;
- oa_overlap_sym: ∀a,b:oa_P.oa_overlap a b → oa_overlap b a;
- oa_meet_inf:
- ∀I:SET.∀p_i:I ⇒ oa_P.∀p:oa_P.
- oa_leq p (oa_meet I p_i) = (∀i:I.oa_leq p (p_i i));
- oa_join_sup: ∀I:SET.∀p_i:I ⇒ oa_P.∀p:oa_P.oa_leq (oa_join I p_i) p = (∀i:I.oa_leq (p_i i) p);
- oa_zero_bot: ∀p:oa_P.oa_leq oa_zero p;
- oa_one_top: ∀p:oa_P.oa_leq p oa_one;
+ oa_leq_refl: ∀a:oa_P. a ≤ a;
+ oa_leq_antisym: ∀a,b:oa_P.a ≤ b → b ≤ a → a = b;
+ oa_leq_trans: ∀a,b,c:oa_P.a ≤ b → b ≤ c → a ≤ c;
+ oa_overlap_sym: ∀a,b:oa_P.a >< b → b >< a;
+ oa_meet_inf: ∀I:SET.∀p_i:I ⇒ oa_P.∀p:oa_P.p ≤ (⋀ p_i) = (∀i:I.p ≤ (p_i i));
+ oa_join_sup: ∀I:SET.∀p_i:I ⇒ oa_P.∀p:oa_P.(⋁ p_i) ≤ p = (∀i:I.p_i i ≤ p);
+ oa_zero_bot: ∀p:oa_P.oa_zero ≤ p;
+ oa_one_top: ∀p:oa_P.p ≤ oa_one;