∀O:ordered_set.∀u,v:O.{[u,v]} square → (bishop_set_of_ordered_set O) square ≝
λO:ordered_set.λu,v:O.λb:{[u,v]} square.〈fst(fst b),fst(snd b)〉.
∀O:ordered_set.∀u,v:O.{[u,v]} square → (bishop_set_of_ordered_set O) square ≝
λO:ordered_set.λu,v:O.λb:{[u,v]} square.〈fst(fst b),fst(snd b)〉.