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

let x be set ; :: thesis: ( x in Y iff x in X \/ (Y \ X) )
( x in Y iff ( x in X or x in Y \ X ) ) by A1, TARSKI:def 3, 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:1; :: thesis: verum