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 that
A1: a in X and
A2: b c= a ; :: thesis: b in X
a = {} by A1, TARSKI:def 1;
hence b in X by A1, A2; :: 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 1 :: 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 that
A3: A c= X and
for a, b being set st a in A & b in A holds
a \/ b in X ; :: thesis: union A in X

now :: thesis: union A in X

per cases ( A = {} or A = {{}} ) by A3, ZFMISC_1:33;

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:25;
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