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

assume AS: Y c= X ; :: thesis: (X \ Y) \/ Y = X

assume AS: Y c= X ; :: thesis: (X \ Y) \/ Y = X

A: now :: thesis: for o being object st o in X holds

o in (X \ Y) \/ Y

o in (X \ Y) \/ Y

let o be object ; :: thesis: ( o in X implies b_{1} in (X \ Y) \/ Y )

assume B: o in X ; :: thesis: b_{1} in (X \ Y) \/ Y

end;assume B: o in X ; :: thesis: b

now :: thesis: for o being object st o in (X \ Y) \/ Y holds

o in X

hence
(X \ Y) \/ Y = X
by A, TARSKI:2; :: thesis: verumo in X

let o be object ; :: thesis: ( o in (X \ Y) \/ Y implies o in X )

assume B: o in (X \ Y) \/ Y ; :: thesis: o in X

end;assume B: o in (X \ Y) \/ Y ; :: thesis: o in X

now :: thesis: o in X

hence
o in X
; :: thesis: verumassume C:
not o in X
; :: thesis: contradiction

then not o in X \ Y ;

then o in Y by B, XBOOLE_0:def 3;

hence contradiction by AS, C; :: thesis: verum

end;then not o in X \ Y ;

then o in Y by B, XBOOLE_0:def 3;

hence contradiction by AS, C; :: thesis: verum