+
+definition bs_subset ≝ λO:bishop_set.λP,Q:O→Prop.∀x:O.P x → Q x.
+
+interpretation "bishop set subset" 'subset a b = (bs_subset _ a b).
+
+definition square_bishop_set : bishop_set → bishop_set.
+intro S; apply (mk_bishop_set (S × S));
+[1: intros (x y); apply ((fst x # fst y) ∨ (snd x # snd y));
+|2: intro x; simplify; intro; cases H (X X); clear H; apply (bs_coreflexive ?? X);
+|3: intros 2 (x y); simplify; intro H; cases H (X X); clear H; [left|right] apply (bs_symmetric ??? X);
+|4: intros 3 (x y z); simplify; intro H; cases H (X X); clear H;
+ [1: cases (bs_cotransitive ??? (fst z) X); [left;left|right;left]assumption;
+ |2: cases (bs_cotransitive ??? (snd z) X); [left;right|right;right]assumption;]]
+qed.
+
+notation "s 2 \atop \neq" non associative with precedence 90
+ for @{ 'square_bs $s }.
+interpretation "bishop set square" 'square x = (square_bishop_set x).
+interpretation "bishop set square" 'square_bs x = (square_bishop_set x).
\ No newline at end of file