interpretation "bishop set apartness" 'apart x y = (bs_apart _ x y).
definition bishop_set_of_ordered_set: ordered_set → bishop_set.
interpretation "bishop set apartness" 'apart x y = (bs_apart _ x y).
definition bishop_set_of_ordered_set: ordered_set → bishop_set.