let X, Y be set ; :: thesis: ( Y c= X implies (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

let o be object ; :: thesis: ( o in X implies b₁ in (X \ Y) \/ Y )
assume B: o in X ; :: thesis: b₁ in (X \ Y) \/ Y

per cases ( o in Y or not o in Y ) ;

suppose o in Y ; :: thesis: b₁ in (X \ Y) \/ Y

hence o in (X \ Y) \/ Y by XBOOLE_0:def 3; :: thesis: verum

end;

suppose not o in Y ; :: thesis: b₁ in (X \ Y) \/ Y

then o in X \ Y by B, XBOOLE_0:def 5;
hence o in (X \ Y) \/ Y by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

now :: thesis: for o being object st o in (X \ Y) \/ Y holds
o 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

now :: thesis: o in X

assume 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;

hence o in X ; :: thesis: verum

end;

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