take X = {{} }; :: thesis: ( X is subset-closed & X is binary_complete & not X is empty )
thus for a, b being set st a in X & b c= a holds
b in X :: according to CLASSES1:def 1 :: thesis: ( X is binary_complete & not X is empty )

proof

let a, b be set ; :: thesis: ( a in X & b c= a implies b in X )
assume A1: ( a in X & b c= a ) ; :: thesis: b in X
then a = {} by TARSKI:def 1;
hence b in X by A1; :: thesis: verum

end;

thus for A being set st A c= X & ( for a, b being set st a in A & b in A holds
a \/ b in X ) holds
union A in X :: according to COH_SP:def 2 :: thesis: not X is empty

proof

let A be set ; :: thesis: ( A c= X & ( for a, b being set st a in A & b in A holds
a \/ b in X ) implies union A in X )
assume A2: ( A c= X & ( for a, b being set st a in A & b in A holds
a \/ b in X ) ) ; :: thesis: union A in X

now

per cases ( A = {} or A = {{} } ) by A2, ZFMISC_1:39;

suppose A = {} ; :: thesis: union A in X

hence union A in X by TARSKI:def 1, ZFMISC_1:2; :: thesis: verum

end;

suppose A = {{} } ; :: thesis: union A in X

then union A = {} by ZFMISC_1:31;
hence union A in X by TARSKI:def 1; :: thesis: verum

end;

end;

end;

hence union A in X ; :: thesis: verum

end;

thus not X is empty ; :: thesis: verum