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