:: deftheorem Def1 defines binary_complete COHSP_1:def 1 :
for X being set holds
( X is binary_complete iff for A being set st ( for a, b being set st a in A & b in A holds
a \/ b in X ) holds
union A in X );