bs_cotransitive: cotransitive ? bs_apart
}.
-notation "hvbox(a break # b)" non associative with precedence 50
+notation "hvbox(a break # b)" non associative with precedence 45
for @{ 'apart $a $b}.
interpretation "bishop_setapartness" 'apart x y = (bs_apart _ x y).
(* Definition 2.2 (2) *)
definition eq ≝ λA:bishop_set.λa,b:A. ¬ (a # b).
-notation "hvbox(a break ≈ b)" non associative with precedence 50
+notation "hvbox(a break ≈ b)" non associative with precedence 45
for @{ 'napart $a $b}.
interpretation "Bishop set alikeness" 'napart a b = (eq _ a b).