boole.miz

    begin

    theorem :: BOOLE:1

    for X be set holds (X \/ {} ) = X

    proof

      let X be set;

      thus (X \/ {} ) c= X

      proof

        let x be object;

        assume x in (X \/ {} );

        then x in X or x in {} by XBOOLE_0:def 3;

        hence thesis by XBOOLE_0:def 1;

      end;

      let x be object;

      assume x in X;

      hence thesis by XBOOLE_0:def 3;

    end;

    theorem :: BOOLE:2

    for X be set holds (X /\ {} ) = {}

    proof

      let X be set;

      thus (X /\ {} ) c= {} by XBOOLE_0:def 4;

      let x be object;

      assume x in {} ;

      hence thesis by XBOOLE_0:def 1;

    end;

    theorem :: BOOLE:3

    for X be set holds (X \ {} ) = X

    proof

      let X be set;

      thus (X \ {} ) c= X by XBOOLE_0:def 5;

      let x be object;



       A1: not x in {} by XBOOLE_0:def 1;

      assume x in X;

      hence thesis by A1, XBOOLE_0:def 5;

    end;

    theorem :: BOOLE:4

    for X be set holds ( {} \ X) = {}

    proof

      let X be set;

      thus ( {} \ X) c= {} by XBOOLE_0:def 5;

      let x be object;

      assume x in {} ;

      hence thesis by XBOOLE_0:def 1;

    end;

    theorem :: BOOLE:5

    for X be set holds (X \+\ {} ) = X

    proof

      let X be set;

      thus (X \+\ {} ) c= X

      proof

        let x be object;

        assume x in (X \+\ {} );

        then

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

        per cases by A1, XBOOLE_0:def 5;

          suppose x in X & not x in {} ;

          hence thesis;

        end;

          suppose x in {} & not x in X;

          hence thesis by XBOOLE_0:def 1;

        end;

      end;

      let x be object;



       A2: not x in {} by XBOOLE_0:def 1;

      assume x in X;

      then x in (X \ {} ) by A2, XBOOLE_0:def 5;

      hence thesis by XBOOLE_0:def 3;

    end;

    reserve x,X for set;



     Lm1: X is empty implies X = {}

    proof

      assume not ex x be object st x in X;

      then for x be object holds x in {} iff x in X by XBOOLE_0:def 1;

      hence thesis by TARSKI: 2;

    end;

    theorem :: BOOLE:6

    for X be set st X is empty holds X = {} by Lm1;

    theorem :: BOOLE:7

    for x,X be set st x in X holds X is non empty by XBOOLE_0:def 1;

    theorem :: BOOLE:8

    for X,Y be set st X is empty & X <> Y holds Y is non empty

    proof

      let X,Y be set;

      assume that

       A1: X is empty and

       A2: X <> Y;

      X = {} by A1, Lm1;

      hence thesis by A2, Lm1;

    end;