thus ( X is binary_complete implies 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 ) :: thesis: ( ( 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 ) implies X is binary_complete )

proof

assume A1: 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: 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
let A be set ; :: thesis: ( ( for a, b being set st a in A & b in A holds
a \/ b in X ) implies union A in X )
assume A2: for a, b being set st a in A & b in A holds
a \/ b in X ; :: thesis: union A in X
A c= X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in X )
reconsider xx = x as set by TARSKI:1;
assume x in A ; :: thesis: x in X
then xx \/ xx in X by A2;
hence x in X ; :: thesis: verum

end;

hence union A in X by A1, A2; :: thesis: verum

end;

assume 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 ; :: thesis: X is binary_complete
hence 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: verum