environ vocabulary BOOLE; notation TARSKI, XBOOLE_0; constructors TARSKI, XBOOLE_0; begin :: This file contains statements which are obvious for Mizar checker if :: "requirements BOOLE" is included in the environment description :: of an article. They are published for testing purposes only. :: Users should use appropriate requirements instead of referencing :: to these theorems. :: Statements which cannot be expressed in Mizar language are commented out. theorem :: BOOLE:1 for X being set holds X \/ {} = X; theorem :: BOOLE:2 for X being set holds X /\ {} = {}; theorem :: BOOLE:3 for X being set holds X \ {} = X; theorem :: BOOLE:4 for X being set holds {} \ X = {}; theorem :: BOOLE:5 for X being set holds X \+\ {} = X; theorem :: BOOLE:6 for X being set st X is empty holds X = {}; theorem :: BOOLE:7 for x, X being set st x in X holds X is non empty; theorem :: BOOLE:8 for X, Y being set st X is empty & X <> Y holds Y is non empty; ::theorem :: equality of 0 and {} is assumed :: 0 is empty; ::theorem :: for X being set holds ::