let X be set ; :: thesis: X \+\ {} = X
thus X \+\ {} c= X :: according to XBOOLE_0:def 10 :: thesis: X c= X \+\ {}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X \+\ {} or x in X )
assume x in X \+\ {} ; :: thesis: x in X
then A1: ( x in X \ {} or x in {} \ X ) by XBOOLE_0:def 3;

per cases ( ( x in X & not x in {} ) or ( x in {} & not x in X ) ) by A1, XBOOLE_0:def 5;

suppose ( x in X & not x in {} ) ; :: thesis: x in X

hence x in X ; :: thesis: verum

end;

suppose ( x in {} & not x in X ) ; :: thesis: x in X

hence x in X by XBOOLE_0:def 1; :: thesis: verum

end;

end;

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in X \+\ {} )
A2: not x in {} by XBOOLE_0:def 1;
assume x in X ; :: thesis: x in X \+\ {}
then x in X \ {} by A2, XBOOLE_0:def 5;
hence x in X \+\ {} by XBOOLE_0:def 3; :: thesis: verum