(* Definition 2.2 (3) *)
definition le ≝ λE:half_ordered_set.λa,b:E. ¬ (a ≰≰ b).
notation "hvbox(a break ≤≤ b)" non associative with precedence 45 for @{ 'leq_low $a $b }.
(* Definition 2.2 (3) *)
definition le ≝ λE:half_ordered_set.λa,b:E. ¬ (a ≰≰ b).
notation "hvbox(a break ≤≤ b)" non associative with precedence 45 for @{ 'leq_low $a $b }.