let X, Y be set ; :: thesis: ( X c= Y implies Y = X \/ (Y \ X) )
assume A1: X c= Y ; :: thesis: Y = X \/ (Y \ X)

now :: thesis: for x being object holds
( x in Y iff x in X \/ (Y \ X) )

let x be object ; :: thesis: ( x in Y iff x in X \/ (Y \ X) )
( x in Y iff ( x in X or x in Y \ X ) ) by A1, XBOOLE_0:def 5;
hence ( x in Y iff x in X \/ (Y \ X) ) by XBOOLE_0:def 3; :: thesis: verum

end;

hence Y = X \/ (Y \ X) by TARSKI:2; :: thesis: verum