let X be set ; :: thesis: X \+\ {} = X

thus X \+\ {} c= X :: according to XBOOLE_0:def 10 :: thesis: X c= 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

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 \+\ {} )
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;

end;assume x in X \+\ {} ; :: thesis: x in X

then A1: ( x in X \ {} or x in {} \ X ) by XBOOLE_0:def 3;

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