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

assume A1: X c= Y ; :: thesis: 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) )

hence
Y = X \/ (Y \ X)
by TARSKI:2; :: thesis: verum( 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;( 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