:: BOOLE semantic presentation begin theorem :: BOOLE:1 for X being set holds X \/ {} = X proof 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 set ; :: 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 set ; :: 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 end; theorem :: BOOLE:2 for X being set holds X /\ {} = {} proof let X be set ; ::_thesis: X /\ {} = {} thus X /\ {} c= {} :: according to XBOOLE_0:def_10 ::_thesis: {} c= X /\ {} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X /\ {} or x in {} ) assume x in X /\ {} ; ::_thesis: x in {} hence x in {} by XBOOLE_0:def_4; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {} or x in X /\ {} ) assume x in {} ; ::_thesis: x in X /\ {} hence x in X /\ {} by XBOOLE_0:def_1; ::_thesis: verum end; theorem :: BOOLE:3 for X being set holds X \ {} = X proof 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 set ; :: 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_5; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in X \ {} ) A1: not x in {} by XBOOLE_0:def_1; assume x in X ; ::_thesis: x in X \ {} hence x in X \ {} by A1, XBOOLE_0:def_5; ::_thesis: verum end; theorem :: BOOLE:4 for X being set holds {} \ X = {} proof let X be set ; ::_thesis: {} \ X = {} thus {} \ X c= {} :: according to XBOOLE_0:def_10 ::_thesis: {} c= {} \ X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {} \ X or x in {} ) assume x in {} \ X ; ::_thesis: x in {} hence x in {} by XBOOLE_0:def_5; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {} or x in {} \ X ) assume x in {} ; ::_thesis: x in {} \ X hence x in {} \ X by XBOOLE_0:def_1; ::_thesis: verum end; theorem :: BOOLE:5 for X being set holds X \+\ {} = X proof 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 set ; :: 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; percases ( ( 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 set ; :: 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 end; Lm1: for X being set st X is empty holds X = {} proof let X be set ; ::_thesis: ( X is empty implies X = {} ) assume for x being set holds not x in X ; :: according to XBOOLE_0:def_1 ::_thesis: X = {} then for x being set holds ( x in {} iff x in X ) by XBOOLE_0:def_1; hence X = {} by TARSKI:1; ::_thesis: verum end; theorem :: BOOLE:6 for X being set st X is empty holds X = {} by Lm1; theorem :: BOOLE:7 for x, X being set st x in X holds not X is empty by XBOOLE_0:def_1; theorem :: BOOLE:8 for X, Y being set st X is empty & X <> Y holds not Y is empty proof let X, Y be set ; ::_thesis: ( X is empty & X <> Y implies not Y is empty ) assume that A1: X is empty and A2: X <> Y ; ::_thesis: not Y is empty X = {} by A1, Lm1; hence not Y is empty by A2, Lm1; ::_thesis: verum end;