(* Definition 2.2 (2) *)
definition eq ≝ λA:bishop_set.λa,b:A. ¬ (a # b).
-notation "hvbox(a break ≈ b)" non associative with precedence 45
+notation "hvbox(a break \approx b)" non associative with precedence 45
for @{ 'napart $a $b}.
interpretation "Bishop set alikeness" 'napart a b = (eq _ a b).
lemma eq_sym:∀E:bishop_set.∀x,y:E.x ≈ y → y ≈ x ≝ eq_sym_.
lemma eq_trans_: ∀E:bishop_set.transitive ? (eq E).
-(* bug. intros k deve fare whd quanto basta *)
intros 6 (E x y z Exy Eyz); intro Axy; cases (bs_cotransitive ???y Axy);
[apply Exy|apply Eyz] assumption.
qed.