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 ( x in X or x in {} ) by XBOOLE_0:def 3;
hence x in X by XBOOLE_0:def 1; :: thesis: verum

end;

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 \/ {}
hence x in X \/ {} by XBOOLE_0:def 3; :: thesis: verum