xboole_1.miz

    begin

    reserve x,A,B,X,X9,Y,Y9,Z,V for set;

    ::$Notion-Name

    theorem :: XBOOLE_1:1

    X c= Y & Y c= Z implies X c= Z;

    theorem :: XBOOLE_1:2

     {} c= X;

    theorem :: XBOOLE_1:3



     Th3: X c= {} implies X = {}

    proof

      assume X c= {} ;

      hence X c= {} & {} c= X;

    end;

    theorem :: XBOOLE_1:4



     Th4: ((X \/ Y) \/ Z) = (X \/ (Y \/ Z))

    proof

      thus ((X \/ Y) \/ Z) c= (X \/ (Y \/ Z))

      proof

        let x be object;

        assume x in ((X \/ Y) \/ Z);

        then x in (X \/ Y) or x in Z by XBOOLE_0:def 3;

        then x in X or x in Y or x in Z by XBOOLE_0:def 3;

        then x in X or x in (Y \/ Z) by XBOOLE_0:def 3;

        hence thesis by XBOOLE_0:def 3;

      end;

      let x be object;

      assume x in (X \/ (Y \/ Z));

      then x in X or x in (Y \/ Z) by XBOOLE_0:def 3;

      then x in X or x in Y or x in Z by XBOOLE_0:def 3;

      then x in (X \/ Y) or x in Z by XBOOLE_0:def 3;

      hence thesis by XBOOLE_0:def 3;

    end;

    theorem :: XBOOLE_1:5

    ((X \/ Y) \/ Z) = ((X \/ Z) \/ (Y \/ Z))

    proof

      ((X \/ Y) \/ Z) = (X \/ ((Z \/ Z) \/ Y)) by Th4

      .= (X \/ (Z \/ (Z \/ Y))) by Th4

      .= ((X \/ Z) \/ (Y \/ Z)) by Th4;

      hence thesis;

    end;

    theorem :: XBOOLE_1:6

    (X \/ (X \/ Y)) = (X \/ Y)

    proof

      (X \/ (X \/ Y)) = ((X \/ X) \/ Y) by Th4

      .= (X \/ Y);

      hence thesis;

    end;

    theorem :: XBOOLE_1:7



     Th7: X c= (X \/ Y) by XBOOLE_0:def 3;

    theorem :: XBOOLE_1:8



     Th8: X c= Z & Y c= Z implies (X \/ Y) c= Z

    proof

      assume

       A1: X c= Z & Y c= Z;

      let x be object;

      assume x in (X \/ Y);

      then x in X or x in Y by XBOOLE_0:def 3;

      hence thesis by A1;

    end;

    theorem :: XBOOLE_1:9

    X c= Y implies (X \/ Z) c= (Y \/ Z)

    proof

      assume

       A1: X c= Y;

      let x be object;

      assume x in (X \/ Z);

      then x in X or x in Z by XBOOLE_0:def 3;

      then x in Y or x in Z by A1;

      hence thesis by XBOOLE_0:def 3;

    end;

    theorem :: XBOOLE_1:10

    X c= Y implies X c= (Z \/ Y)

    proof

      Y c= (Z \/ Y) by Th7;

      hence thesis;

    end;

    theorem :: XBOOLE_1:11

    (X \/ Y) c= Z implies X c= Z

    proof

      X c= (X \/ Y) by Th7;

      hence thesis;

    end;

    theorem :: XBOOLE_1:12



     Th12: X c= Y implies (X \/ Y) = Y

    proof

      assume

       A1: X c= Y;

      thus (X \/ Y) c= Y

      proof

        let x be object;

        assume x in (X \/ Y);

        then x in X or x in Y by XBOOLE_0:def 3;

        hence thesis by A1;

      end;

      let x be object;

      thus thesis by XBOOLE_0:def 3;

    end;

    theorem :: XBOOLE_1:13

    X c= Y & Z c= V implies (X \/ Z) c= (Y \/ V)

    proof

      assume

       A1: X c= Y;

      assume

       A2: Z c= V;

      let x be object;

      assume x in (X \/ Z);

      then x in X or x in Z by XBOOLE_0:def 3;

      then x in Y or x in V by A1, A2;

      hence thesis by XBOOLE_0:def 3;

    end;

    theorem :: XBOOLE_1:14

    (Y c= X & Z c= X & for V st Y c= V & Z c= V holds X c= V) implies X = (Y \/ Z)

    proof

      assume that

       A1: Y c= X & Z c= X and

       A2: Y c= V & Z c= V implies X c= V;

      Y c= (Y \/ Z) & Z c= (Y \/ Z) by Th7;

      hence X c= (Y \/ Z) by A2;

      thus thesis by A1, Th8;

    end;

    theorem :: XBOOLE_1:15

    (X \/ Y) = {} implies X = {} ;

    theorem :: XBOOLE_1:16



     Th16: ((X /\ Y) /\ Z) = (X /\ (Y /\ Z))

    proof

      thus ((X /\ Y) /\ Z) c= (X /\ (Y /\ Z))

      proof

        let x be object;

        assume

         A1: x in ((X /\ Y) /\ Z);

        then

         A2: x in Z by XBOOLE_0:def 4;



         A3: x in (X /\ Y) by A1, XBOOLE_0:def 4;

        then

         A4: x in X by XBOOLE_0:def 4;

        x in Y by A3, XBOOLE_0:def 4;

        then x in (Y /\ Z) by A2, XBOOLE_0:def 4;

        hence thesis by A4, XBOOLE_0:def 4;

      end;

      let x be object;

      assume

       A5: x in (X /\ (Y /\ Z));

      then

       A6: x in (Y /\ Z) by XBOOLE_0:def 4;

      then

       A7: x in Y by XBOOLE_0:def 4;



       A8: x in Z by A6, XBOOLE_0:def 4;

      x in X by A5, XBOOLE_0:def 4;

      then x in (X /\ Y) by A7, XBOOLE_0:def 4;

      hence thesis by A8, XBOOLE_0:def 4;

    end;

    theorem :: XBOOLE_1:17



     Th17: (X /\ Y) c= X by XBOOLE_0:def 4;

    theorem :: XBOOLE_1:18

    X c= (Y /\ Z) implies X c= Y

    proof

      (Y /\ Z) c= Y by Th17;

      hence thesis;

    end;

    theorem :: XBOOLE_1:19



     Th19: Z c= X & Z c= Y implies Z c= (X /\ Y)

    proof

      assume

       A1: Z c= X & Z c= Y;

      let x be object;

      assume x in Z;

      then x in X & x in Y by A1;

      hence thesis by XBOOLE_0:def 4;

    end;

    theorem :: XBOOLE_1:20

    (X c= Y & X c= Z & for V st V c= Y & V c= Z holds V c= X) implies X = (Y /\ Z)

    proof

      assume that

       A1: X c= Y & X c= Z and

       A2: V c= Y & V c= Z implies V c= X;

      thus X c= (Y /\ Z) by A1, Th19;

      (Y /\ Z) c= Y & (Y /\ Z) c= Z implies (Y /\ Z) c= X by A2;

      hence thesis by Th17;

    end;

    theorem :: XBOOLE_1:21

    (X /\ (X \/ Y)) = X

    proof

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

      let x be object;

      assume

       A1: x in X;

      then x in (X \/ Y) by XBOOLE_0:def 3;

      hence thesis by A1, XBOOLE_0:def 4;

    end;

    theorem :: XBOOLE_1:22



     Th22: (X \/ (X /\ Y)) = X

    proof

      thus (X \/ (X /\ Y)) c= X

      proof

        let x be object;

        assume x in (X \/ (X /\ Y));

        then x in X or x in (X /\ Y) by XBOOLE_0:def 3;

        hence thesis by XBOOLE_0:def 4;

      end;

      let x be object;

      thus thesis by XBOOLE_0:def 3;

    end;

    theorem :: XBOOLE_1:23



     Th23: (X /\ (Y \/ Z)) = ((X /\ Y) \/ (X /\ Z))

    proof

      thus (X /\ (Y \/ Z)) c= ((X /\ Y) \/ (X /\ Z))

      proof

        let x be object;

        assume

         A1: x in (X /\ (Y \/ Z));

        then x in (Y \/ Z) by XBOOLE_0:def 4;

        then

         A2: x in Y or x in Z by XBOOLE_0:def 3;

        x in X by A1, XBOOLE_0:def 4;

        then x in (X /\ Y) or x in (X /\ Z) by A2, XBOOLE_0:def 4;

        hence thesis by XBOOLE_0:def 3;

      end;

      let x be object;

      assume x in ((X /\ Y) \/ (X /\ Z));

      then x in (X /\ Y) or x in (X /\ Z) by XBOOLE_0:def 3;

      then

       A3: x in X & x in Y or x in X & x in Z by XBOOLE_0:def 4;

      then x in (Y \/ Z) by XBOOLE_0:def 3;

      hence thesis by A3, XBOOLE_0:def 4;

    end;

    theorem :: XBOOLE_1:24



     Th24: (X \/ (Y /\ Z)) = ((X \/ Y) /\ (X \/ Z))

    proof

      thus (X \/ (Y /\ Z)) c= ((X \/ Y) /\ (X \/ Z))

      proof

        let x be object;

        assume x in (X \/ (Y /\ Z));

        then x in X or x in (Y /\ Z) by XBOOLE_0:def 3;

        then x in X or x in Y & x in Z by XBOOLE_0:def 4;

        then x in (X \/ Y) & x in (X \/ Z) by XBOOLE_0:def 3;

        hence thesis by XBOOLE_0:def 4;

      end;

      let x be object;

      assume

       A1: x in ((X \/ Y) /\ (X \/ Z));

      then x in (X \/ Z) by XBOOLE_0:def 4;

      then

       A2: x in X or x in Z by XBOOLE_0:def 3;

      x in (X \/ Y) by A1, XBOOLE_0:def 4;

      then x in X or x in Y by XBOOLE_0:def 3;

      then x in X or x in (Y /\ Z) by A2, XBOOLE_0:def 4;

      hence thesis by XBOOLE_0:def 3;

    end;

    theorem :: XBOOLE_1:25

    (((X /\ Y) \/ (Y /\ Z)) \/ (Z /\ X)) = (((X \/ Y) /\ (Y \/ Z)) /\ (Z \/ X))

    proof



      thus (((X /\ Y) \/ (Y /\ Z)) \/ (Z /\ X)) = ((((X /\ Y) \/ (Y /\ Z)) \/ Z) /\ (((X /\ Y) \/ (Y /\ Z)) \/ X)) by Th24

      .= (((X /\ Y) \/ ((Y /\ Z) \/ Z)) /\ (((X /\ Y) \/ (Y /\ Z)) \/ X)) by Th4

      .= (((X /\ Y) \/ Z) /\ (((X /\ Y) \/ (Y /\ Z)) \/ X)) by Th22

      .= (((X /\ Y) \/ Z) /\ (((X /\ Y) \/ X) \/ (Y /\ Z))) by Th4

      .= (((X /\ Y) \/ Z) /\ (X \/ (Y /\ Z))) by Th22

      .= (((X \/ Z) /\ (Y \/ Z)) /\ (X \/ (Y /\ Z))) by Th24

      .= (((X \/ Z) /\ (Y \/ Z)) /\ ((X \/ Y) /\ (X \/ Z))) by Th24

      .= ((X \/ Y) /\ (((Y \/ Z) /\ (X \/ Z)) /\ (X \/ Z))) by Th16

      .= ((X \/ Y) /\ ((Y \/ Z) /\ ((X \/ Z) /\ (X \/ Z)))) by Th16

      .= (((X \/ Y) /\ (Y \/ Z)) /\ (Z \/ X)) by Th16;

    end;

    theorem :: XBOOLE_1:26



     Th26: X c= Y implies (X /\ Z) c= (Y /\ Z)

    proof

      assume

       A1: X c= Y;

      let x be object;

      assume

       A2: x in (X /\ Z);

      then x in X by XBOOLE_0:def 4;

      then

       A3: x in Y by A1;

      x in Z by A2, XBOOLE_0:def 4;

      hence thesis by A3, XBOOLE_0:def 4;

    end;

    theorem :: XBOOLE_1:27

    X c= Y & Z c= V implies (X /\ Z) c= (Y /\ V)

    proof

      assume that

       A1: X c= Y and

       A2: Z c= V;

      let x be object;

      assume

       A3: x in (X /\ Z);

      then x in Z by XBOOLE_0:def 4;

      then

       A4: x in V by A2;

      x in X by A3, XBOOLE_0:def 4;

      then x in Y by A1;

      hence thesis by A4, XBOOLE_0:def 4;

    end;

    theorem :: XBOOLE_1:28



     Th28: X c= Y implies (X /\ Y) = X

    proof

      assume

       A1: X c= Y;

      thus (X /\ Y) c= X by Th17;

      let x be object;

      assume

       A2: x in X;

      then x in Y by A1;

      hence thesis by A2, XBOOLE_0:def 4;

    end;

    theorem :: XBOOLE_1:29

    (X /\ Y) c= (X \/ Z)

    proof

      (X /\ Y) c= X & X c= (X \/ Z) by Th7, Th17;

      hence thesis;

    end;

    theorem :: XBOOLE_1:30

    X c= Z implies (X \/ (Y /\ Z)) = ((X \/ Y) /\ Z)

    proof

      assume

       A1: X c= Z;

      thus (X \/ (Y /\ Z)) c= ((X \/ Y) /\ Z)

      proof

        let x be object;

        assume x in (X \/ (Y /\ Z));

        then

         A2: x in X or x in (Y /\ Z) by XBOOLE_0:def 3;

        then x in X or x in Y & x in Z by XBOOLE_0:def 4;

        then

         A3: x in (X \/ Y) by XBOOLE_0:def 3;

        x in Z by A1, A2, XBOOLE_0:def 4;

        hence thesis by A3, XBOOLE_0:def 4;

      end;

      let x be object;

      assume

       A4: x in ((X \/ Y) /\ Z);

      then x in (X \/ Y) by XBOOLE_0:def 4;

      then

       A5: x in X or x in Y by XBOOLE_0:def 3;

      x in Z by A4, XBOOLE_0:def 4;

      then x in X & x in Z or x in (Y /\ Z) by A5, XBOOLE_0:def 4;

      hence thesis by XBOOLE_0:def 3;

    end;

    theorem :: XBOOLE_1:31

    ((X /\ Y) \/ (X /\ Z)) c= (Y \/ Z)

    proof

      now

        let x be object;

        assume x in ((X /\ Y) \/ (X /\ Z));

        then x in (X /\ Y) or x in (X /\ Z) by XBOOLE_0:def 3;

        then x in X & x in Y or x in X & x in Z by XBOOLE_0:def 4;

        hence x in (Y \/ Z) by XBOOLE_0:def 3;

      end;

      hence thesis;

    end;



     Lm1: (X \ Y) = {} iff X c= Y

    proof

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

      assume

       A1: X c= Y;

      now

        let x be object;

        x in X & not x in Y iff contradiction by A1;

        hence x in (X \ Y) iff x in {} by XBOOLE_0:def 5;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: XBOOLE_1:32

    (X \ Y) = (Y \ X) implies X = Y

    proof

      assume

       A1: (X \ Y) = (Y \ X);

      now

        let x be object;

        x in X & not x in Y iff x in (Y \ X) by A1, XBOOLE_0:def 5;

        hence x in X iff x in Y by XBOOLE_0:def 5;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: XBOOLE_1:33



     Th33: X c= Y implies (X \ Z) c= (Y \ Z)

    proof

      assume

       A1: X c= Y;

      let x be object;

      assume

       A2: x in (X \ Z);

      then x in X by XBOOLE_0:def 5;

      then

       A3: x in Y by A1;

       not x in Z by A2, XBOOLE_0:def 5;

      hence thesis by A3, XBOOLE_0:def 5;

    end;

    theorem :: XBOOLE_1:34



     Th34: X c= Y implies (Z \ Y) c= (Z \ X)

    proof

      assume

       A1: X c= Y;

      let x be object;

      assume

       A2: x in (Z \ Y);

      then not x in Y by XBOOLE_0:def 5;

      then

       A3: not x in X by A1;

      x in Z by A2, XBOOLE_0:def 5;

      hence thesis by A3, XBOOLE_0:def 5;

    end;



     Lm2: (X \ (Y /\ Z)) = ((X \ Y) \/ (X \ Z))

    proof

      thus (X \ (Y /\ Z)) c= ((X \ Y) \/ (X \ Z))

      proof

        let x be object;

        assume

         A1: x in (X \ (Y /\ Z));

        then not x in (Y /\ Z) by XBOOLE_0:def 5;

        then

         A2: not x in Y or not x in Z by XBOOLE_0:def 4;

        x in X by A1, XBOOLE_0:def 5;

        then x in (X \ Y) or x in (X \ Z) by A2, XBOOLE_0:def 5;

        hence thesis by XBOOLE_0:def 3;

      end;

      (X \ Y) c= (X \ (Y /\ Z)) & (X \ Z) c= (X \ (Y /\ Z)) by Th17, Th34;

      hence thesis by Th8;

    end;

    theorem :: XBOOLE_1:35

    X c= Y & Z c= V implies (X \ V) c= (Y \ Z)

    proof

      assume X c= Y & Z c= V;

      then (X \ V) c= (Y \ V) & (Y \ V) c= (Y \ Z) by Th33, Th34;

      hence thesis;

    end;

    theorem :: XBOOLE_1:36



     Th36: (X \ Y) c= X by XBOOLE_0:def 5;

    theorem :: XBOOLE_1:37

    (X \ Y) = {} iff X c= Y by Lm1;

    theorem :: XBOOLE_1:38

    X c= (Y \ X) implies X = {}

    proof

      assume

       A1: X c= (Y \ X);

      thus X c= {}

      proof

        let x be object;

        assume

         A2: x in X;

        then x in (Y \ X) by A1;

        hence thesis by A2, XBOOLE_0:def 5;

      end;

      thus thesis;

    end;

    theorem :: XBOOLE_1:39



     Th39: (X \/ (Y \ X)) = (X \/ Y)

    proof

      thus (X \/ (Y \ X)) c= (X \/ Y)

      proof

        let x be object;

        assume x in (X \/ (Y \ X));

        then x in X or x in (Y \ X) by XBOOLE_0:def 3;

        then x in X or x in Y by XBOOLE_0:def 5;

        hence thesis by XBOOLE_0:def 3;

      end;

      let x be object;

      assume x in (X \/ Y);

      then x in X or x in Y & not x in X by XBOOLE_0:def 3;

      then x in X or x in (Y \ X) by XBOOLE_0:def 5;

      hence thesis by XBOOLE_0:def 3;

    end;

    theorem :: XBOOLE_1:40

    ((X \/ Y) \ Y) = (X \ Y)

    proof

      thus for x be object holds x in ((X \/ Y) \ Y) implies x in (X \ Y)

      proof

        let x be object;

        assume

         A1: x in ((X \/ Y) \ Y);

        then x in (X \/ Y) by XBOOLE_0:def 5;

        then

         A2: x in X or x in Y by XBOOLE_0:def 3;

         not x in Y by A1, XBOOLE_0:def 5;

        hence thesis by A2, XBOOLE_0:def 5;

      end;

      thus for x be object holds x in (X \ Y) implies x in ((X \/ Y) \ Y)

      proof

        let x be object;

        assume

         A3: x in (X \ Y);

        then x in X or x in Y by XBOOLE_0:def 5;

        then

         A4: x in (X \/ Y) by XBOOLE_0:def 3;

         not x in Y by A3, XBOOLE_0:def 5;

        hence thesis by A4, XBOOLE_0:def 5;

      end;

    end;

    theorem :: XBOOLE_1:41



     Th41: ((X \ Y) \ Z) = (X \ (Y \/ Z))

    proof

      thus for x be object holds x in ((X \ Y) \ Z) implies x in (X \ (Y \/ Z))

      proof

        let x be object;

        assume

         A1: x in ((X \ Y) \ Z);

        then

         A2: not x in Z by XBOOLE_0:def 5;



         A3: x in (X \ Y) by A1, XBOOLE_0:def 5;

        then

         A4: x in X by XBOOLE_0:def 5;

         not x in Y by A3, XBOOLE_0:def 5;

        then not x in (Y \/ Z) by A2, XBOOLE_0:def 3;

        hence thesis by A4, XBOOLE_0:def 5;

      end;

      thus for x be object holds x in (X \ (Y \/ Z)) implies x in ((X \ Y) \ Z)

      proof

        let x be object;

        assume

         A5: x in (X \ (Y \/ Z));

        then

         A6: not x in (Y \/ Z) by XBOOLE_0:def 5;

        then

         A7: not x in Y by XBOOLE_0:def 3;



         A8: not x in Z by A6, XBOOLE_0:def 3;

        x in X by A5, XBOOLE_0:def 5;

        then x in (X \ Y) by A7, XBOOLE_0:def 5;

        hence thesis by A8, XBOOLE_0:def 5;

      end;

    end;

    theorem :: XBOOLE_1:42



     Th42: ((X \/ Y) \ Z) = ((X \ Z) \/ (Y \ Z))

    proof

      thus ((X \/ Y) \ Z) c= ((X \ Z) \/ (Y \ Z))

      proof

        let x be object;

        assume

         A1: x in ((X \/ Y) \ Z);

        then x in (X \/ Y) by XBOOLE_0:def 5;

        then x in X & not x in Z or x in Y & not x in Z by A1, XBOOLE_0:def 3, XBOOLE_0:def 5;

        then x in (X \ Z) or x in (Y \ Z) by XBOOLE_0:def 5;

        hence thesis by XBOOLE_0:def 3;

      end;

      let x be object;

      assume x in ((X \ Z) \/ (Y \ Z));

      then x in (X \ Z) or x in (Y \ Z) by XBOOLE_0:def 3;

      then

       A2: x in X & not x in Z or x in Y & not x in Z by XBOOLE_0:def 5;

      then x in (X \/ Y) by XBOOLE_0:def 3;

      hence thesis by A2, XBOOLE_0:def 5;

    end;

    theorem :: XBOOLE_1:43

    X c= (Y \/ Z) implies (X \ Y) c= Z

    proof

      assume

       A1: X c= (Y \/ Z);

      let x be object;

      assume

       A2: x in (X \ Y);

      then x in X by XBOOLE_0:def 5;

      then

       A3: x in (Y \/ Z) by A1;

       not x in Y by A2, XBOOLE_0:def 5;

      hence thesis by A3, XBOOLE_0:def 3;

    end;

    theorem :: XBOOLE_1:44

    (X \ Y) c= Z implies X c= (Y \/ Z)

    proof

      assume

       A1: for x be object holds x in (X \ Y) implies x in Z;

      let x be object;

      assume x in X;

      then x in (X \ Y) or x in Y by XBOOLE_0:def 5;

      then x in Z or x in Y by A1;

      hence thesis by XBOOLE_0:def 3;

    end;

    theorem :: XBOOLE_1:45

    X c= Y implies Y = (X \/ (Y \ X))

    proof

      assume

       A1: X c= Y;

      now

        let x be object;

        x in Y iff x in X or x in (Y \ X) by A1, XBOOLE_0:def 5;

        hence x in Y iff x in (X \/ (Y \ X)) by XBOOLE_0:def 3;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: XBOOLE_1:46

    (X \ (X \/ Y)) = {} by Th7, Lm1;

    theorem :: XBOOLE_1:47



     Th47: (X \ (X /\ Y)) = (X \ Y)

    proof

      now

        let x be object;

        x in X & not x in (X /\ Y) iff x in X & not x in Y by XBOOLE_0:def 4;

        hence x in (X \ (X /\ Y)) iff x in (X \ Y) by XBOOLE_0:def 5;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: XBOOLE_1:48

    (X \ (X \ Y)) = (X /\ Y)

    proof

      thus for x be object holds x in (X \ (X \ Y)) implies x in (X /\ Y)

      proof

        let x be object;

        assume

         A1: x in (X \ (X \ Y));

        then not x in (X \ Y) by XBOOLE_0:def 5;

        then

         A2: not x in X or x in Y by XBOOLE_0:def 5;

        x in X by A1, XBOOLE_0:def 5;

        hence thesis by A2, XBOOLE_0:def 4;

      end;

      thus for x be object holds x in (X /\ Y) implies x in (X \ (X \ Y))

      proof

        let x be object;

        assume

         A3: x in (X /\ Y);

        then not x in X or x in Y by XBOOLE_0:def 4;

        then

         A4: not x in (X \ Y) by XBOOLE_0:def 5;

        x in X by A3, XBOOLE_0:def 4;

        hence thesis by A4, XBOOLE_0:def 5;

      end;

    end;

    theorem :: XBOOLE_1:49



     Th49: (X /\ (Y \ Z)) = ((X /\ Y) \ Z)

    proof

      now

        let x be object;

        x in X & x in Y & not x in Z iff x in X & x in Y & not x in Z;

        then x in X & x in (Y \ Z) iff x in (X /\ Y) & not x in Z by XBOOLE_0:def 4, XBOOLE_0:def 5;

        hence x in (X /\ (Y \ Z)) iff x in ((X /\ Y) \ Z) by XBOOLE_0:def 4, XBOOLE_0:def 5;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: XBOOLE_1:50



     Th50: (X /\ (Y \ Z)) = ((X /\ Y) \ (X /\ Z))

    proof



       A1: (X /\ Y) c= X by Th17;

      ((X /\ Y) \ (X /\ Z)) = (((X /\ Y) \ X) \/ ((X /\ Y) \ Z)) by Lm2

      .= ( {} \/ ((X /\ Y) \ Z)) by A1, Lm1

      .= ((X /\ Y) \ Z);

      hence thesis by Th49;

    end;

    theorem :: XBOOLE_1:51



     Th51: ((X /\ Y) \/ (X \ Y)) = X

    proof

      thus ((X /\ Y) \/ (X \ Y)) c= X

      proof

        let x be object;

        assume x in ((X /\ Y) \/ (X \ Y));

        then x in (X /\ Y) or x in (X \ Y) by XBOOLE_0:def 3;

        hence thesis by XBOOLE_0:def 4, XBOOLE_0:def 5;

      end;

      let x be object;

      assume x in X;

      then x in X & x in Y or x in (X \ Y) by XBOOLE_0:def 5;

      then x in (X /\ Y) or x in (X \ Y) by XBOOLE_0:def 4;

      hence thesis by XBOOLE_0:def 3;

    end;

    theorem :: XBOOLE_1:52



     Th52: (X \ (Y \ Z)) = ((X \ Y) \/ (X /\ Z))

    proof

      thus for x be object holds x in (X \ (Y \ Z)) implies x in ((X \ Y) \/ (X /\ Z))

      proof

        let x be object;

        assume

         A1: x in (X \ (Y \ Z));

        then not x in (Y \ Z) by XBOOLE_0:def 5;

        then x in X & not x in Y or x in X & x in Z by A1, XBOOLE_0:def 5;

        then x in (X \ Y) or x in (X /\ Z) by XBOOLE_0:def 4, XBOOLE_0:def 5;

        hence thesis by XBOOLE_0:def 3;

      end;

      let x be object;

      assume x in ((X \ Y) \/ (X /\ Z));

      then x in (X \ Y) or x in (X /\ Z) by XBOOLE_0:def 3;

      then

       A2: x in X & not x in Y or x in X & x in Z by XBOOLE_0:def 4, XBOOLE_0:def 5;

      then not x in (Y \ Z) by XBOOLE_0:def 5;

      hence thesis by A2, XBOOLE_0:def 5;

    end;

    theorem :: XBOOLE_1:53

    (X \ (Y \/ Z)) = ((X \ Y) /\ (X \ Z))

    proof

      (X \ (Y \/ Z)) c= (X \ Y) & (X \ (Y \/ Z)) c= (X \ Z) by Th7, Th34;

      hence (X \ (Y \/ Z)) c= ((X \ Y) /\ (X \ Z)) by Th19;

      let x be object;

      assume

       A1: x in ((X \ Y) /\ (X \ Z));

      then

       A2: x in (X \ Y) by XBOOLE_0:def 4;

      then

       A3: x in X by XBOOLE_0:def 5;

      x in (X \ Z) by A1, XBOOLE_0:def 4;

      then

       A4: not x in Z by XBOOLE_0:def 5;

       not x in Y by A2, XBOOLE_0:def 5;

      then not x in (Y \/ Z) by A4, XBOOLE_0:def 3;

      hence thesis by A3, XBOOLE_0:def 5;

    end;

    theorem :: XBOOLE_1:54

    (X \ (Y /\ Z)) = ((X \ Y) \/ (X \ Z)) by Lm2;

    theorem :: XBOOLE_1:55



     Th55: ((X \/ Y) \ (X /\ Y)) = ((X \ Y) \/ (Y \ X))

    proof

      for x be object holds x in ((X \/ Y) \ (X /\ Y)) iff x in ((X \ Y) \/ (Y \ X))

      proof

        let x be object;

        thus x in ((X \/ Y) \ (X /\ Y)) implies x in ((X \ Y) \/ (Y \ X))

        proof

          assume

           A1: x in ((X \/ Y) \ (X /\ Y));

          then not x in (X /\ Y) by XBOOLE_0:def 5;

          then

           A2: not x in X or not x in Y by XBOOLE_0:def 4;

          x in (X \/ Y) by A1, XBOOLE_0:def 5;

          then x in X or x in Y by XBOOLE_0:def 3;

          then x in (X \ Y) or x in (Y \ X) by A2, XBOOLE_0:def 5;

          hence thesis by XBOOLE_0:def 3;

        end;

        assume x in ((X \ Y) \/ (Y \ X));

        then x in (X \ Y) or x in (Y \ X) by XBOOLE_0:def 3;

        then x in X & not x in Y or x in Y & not x in X by XBOOLE_0:def 5;

        then ( not x in (X /\ Y)) & x in (X \/ Y) by XBOOLE_0:def 3, XBOOLE_0:def 4;

        hence thesis by XBOOLE_0:def 5;

      end;

      hence thesis by TARSKI: 2;

    end;



     Lm3: X c= Y & Y c< Z implies X c< Z

    proof

      assume that

       A1: X c= Y and

       A2: Y c< Z;

      Y c= Z by A2;

      hence X c= Z & X <> Z by A1, A2, XBOOLE_0:def 10;

    end;

    theorem :: XBOOLE_1:56

    X c< Y & Y c< Z implies X c< Z by Lm3;

    theorem :: XBOOLE_1:57

     not (X c< Y & Y c< X);

    theorem :: XBOOLE_1:58

    X c< Y & Y c= Z implies X c< Z

    proof

      assume that

       A1: X c< Y and

       A2: Y c= Z;

      X c= Y by A1;

      hence X c= Z & X <> Z by A1, A2, XBOOLE_0:def 10;

    end;

    theorem :: XBOOLE_1:59

    X c= Y & Y c< Z implies X c< Z by Lm3;

    theorem :: XBOOLE_1:60



     Th60: X c= Y implies not Y c< X

    proof

      assume X c= Y & Y c= X & X <> Y;

      hence contradiction;

    end;

    theorem :: XBOOLE_1:61

    X <> {} implies {} c< X

    proof

      assume

       A1: X <> {} ;

      thus {} c= X;

      thus thesis by A1;

    end;

    theorem :: XBOOLE_1:62

     not X c< {} by Th3;

    ::$Notion-Name

    ::$Notion-Name

    theorem :: XBOOLE_1:63



     Th63: X c= Y & Y misses Z implies X misses Z by Th3, Th26;

    theorem :: XBOOLE_1:64

    A c= X & B c= Y & X misses Y implies A misses B

    proof

      assume that

       A1: A c= X and

       A2: B c= Y and

       A3: X misses Y;

      A misses Y by A1, A3, Th63;

      hence thesis by A2, Th63;

    end;

    theorem :: XBOOLE_1:65

    X misses {} ;

    theorem :: XBOOLE_1:66

    X meets X iff X <> {} ;

    theorem :: XBOOLE_1:67

    X c= Y & X c= Z & Y misses Z implies X = {} by Th3, Th19;

    ::$Notion-Name

    theorem :: XBOOLE_1:68



     Th68: for A be non empty set st A c= Y & A c= Z holds Y meets Z

    proof

      let A be non empty set;

      consider x be object such that

       A1: x in A by XBOOLE_0:def 1;

      assume A c= Y & A c= Z;

      then x in Y & x in Z by A1;

      hence thesis by XBOOLE_0: 3;

    end;

    theorem :: XBOOLE_1:69

    for A be non empty set st A c= Y holds A meets Y by Th68;

    theorem :: XBOOLE_1:70



     Th70: X meets (Y \/ Z) iff X meets Y or X meets Z

    proof

      thus X meets (Y \/ Z) implies X meets Y or X meets Z

      proof

        assume X meets (Y \/ Z);

        then

        consider x be object such that

         A1: x in X & x in (Y \/ Z) by XBOOLE_0: 3;

        x in X & x in Y or x in X & x in Z by A1, XBOOLE_0:def 3;

        hence thesis by XBOOLE_0: 3;

      end;



       A2: X meets Z implies X meets (Y \/ Z)

      proof

        assume X meets Z;

        then

        consider x be object such that

         A3: x in X and

         A4: x in Z by XBOOLE_0: 3;

        x in (Y \/ Z) by A4, XBOOLE_0:def 3;

        hence thesis by A3, XBOOLE_0: 3;

      end;

      X meets Y implies X meets (Y \/ Z)

      proof

        assume X meets Y;

        then

        consider x be object such that

         A5: x in X and

         A6: x in Y by XBOOLE_0: 3;

        x in (Y \/ Z) by A6, XBOOLE_0:def 3;

        hence thesis by A5, XBOOLE_0: 3;

      end;

      hence thesis by A2;

    end;

    theorem :: XBOOLE_1:71

    (X \/ Y) = (Z \/ Y) & X misses Y & Z misses Y implies X = Z

    proof

      assume that

       A1: (X \/ Y) = (Z \/ Y) and

       A2: (X /\ Y) = {} and

       A3: (Z /\ Y) = {} ;

      thus X c= Z

      proof

        let x be object such that

         A4: x in X;

        X c= (Z \/ Y) by A1, Th7;

        then

         A5: x in (Z \/ Y) by A4;

         not x in Y by A2, A4, XBOOLE_0:def 4;

        hence thesis by A5, XBOOLE_0:def 3;

      end;

      let x be object such that

       A6: x in Z;

      Z c= (X \/ Y) by A1, Th7;

      then

       A7: x in (X \/ Y) by A6;

       not x in Y by A3, A6, XBOOLE_0:def 4;

      hence thesis by A7, XBOOLE_0:def 3;

    end;

    theorem :: XBOOLE_1:72

    (X9 \/ Y9) = (X \/ Y) & X misses X9 & Y misses Y9 implies X = Y9

    proof

      assume

       A1: (X9 \/ Y9) = (X \/ Y);

      assume X misses X9 & Y misses Y9;

      then

       A2: (X /\ X9) = {} & (Y /\ Y9) = {} ;



      thus X = (X /\ (X9 \/ Y9)) by A1, Th7, Th28

      .= ((X /\ X9) \/ (X /\ Y9)) by Th23

      .= ((X \/ Y) /\ Y9) by A2, Th23

      .= Y9 by A1, Th7, Th28;

    end;

    theorem :: XBOOLE_1:73

    X c= (Y \/ Z) & X misses Z implies X c= Y

    proof

      assume that

       A1: X c= (Y \/ Z) and

       A2: (X /\ Z) = {} ;

      (X /\ (Y \/ Z)) = X by A1, Th28;

      then ((Y /\ X) \/ {} ) = X by A2, Th23;

      hence thesis by Th17;

    end;

    theorem :: XBOOLE_1:74



     Th74: X meets (Y /\ Z) implies X meets Y

    proof

      assume X meets (Y /\ Z);

      then

      consider x be object such that

       A1: x in X and

       A2: x in (Y /\ Z) by XBOOLE_0: 3;

      x in Y by A2, XBOOLE_0:def 4;

      hence thesis by A1, XBOOLE_0: 3;

    end;

    theorem :: XBOOLE_1:75

    X meets Y implies (X /\ Y) meets Y

    proof

      assume X meets Y;

      then

      consider x be object such that

       A1: x in X and

       A2: x in Y by XBOOLE_0: 3;

      x in (X /\ Y) by A1, A2, XBOOLE_0:def 4;

      hence thesis by A2, XBOOLE_0: 3;

    end;

    theorem :: XBOOLE_1:76

    Y misses Z implies (X /\ Y) misses (X /\ Z)

    proof

      assume Y misses Z;

      then (X /\ Z) misses Y by Th74;

      hence thesis by Th74;

    end;

    theorem :: XBOOLE_1:77

    X meets Y & X c= Z implies X meets (Y /\ Z)

    proof

      assume that

       A1: X meets Y and

       A2: X c= Z;

      now

        assume

         A3: (X /\ (Y /\ Z)) = {} ;

        (X /\ Y) = ((X /\ Z) /\ Y) by A2, Th28

        .= {} by A3, Th16;

        hence contradiction by A1;

      end;

      hence thesis;

    end;

    theorem :: XBOOLE_1:78

    X misses Y implies (X /\ (Y \/ Z)) = (X /\ Z)

    proof

      assume X misses Y;

      then (X /\ Y) = {} ;



      hence (X /\ (Y \/ Z)) = ( {} \/ (X /\ Z)) by Th23

      .= (X /\ Z);

    end;

    theorem :: XBOOLE_1:79



     Th79: (X \ Y) misses Y

    proof

       not ex x be object st x in ((X \ Y) /\ Y)

      proof

        given x be object such that

         A1: x in ((X \ Y) /\ Y);

        x in (X \ Y) & x in Y by A1, XBOOLE_0:def 4;

        hence contradiction by XBOOLE_0:def 5;

      end;

      hence ((X \ Y) /\ Y) = {} by XBOOLE_0:def 1;

    end;

    theorem :: XBOOLE_1:80

    X misses Y implies X misses (Y \ Z)

    proof

      assume

       A1: X misses Y;

      assume X meets (Y \ Z);

      then

      consider x be object such that

       A2: x in X and

       A3: x in (Y \ Z) by XBOOLE_0: 3;

      x in Y by A3, XBOOLE_0:def 5;

      hence thesis by A1, A2, XBOOLE_0: 3;

    end;

    theorem :: XBOOLE_1:81

    X misses (Y \ Z) implies Y misses (X \ Z)

    proof

      (X /\ (Y \ Z)) = ((Y /\ X) \ Z) by Th49

      .= (Y /\ (X \ Z)) by Th49;

      hence thesis;

    end;

    theorem :: XBOOLE_1:82

    (X \ Y) misses (Y \ X)

    proof

      assume (X \ Y) meets (Y \ X);

      then

      consider x be object such that

       A1: x in (X \ Y) and

       A2: x in (Y \ X) by XBOOLE_0: 3;

      x in X by A1, XBOOLE_0:def 5;

      hence thesis by A2, XBOOLE_0:def 5;

    end;

    theorem :: XBOOLE_1:83



     Th83: X misses Y iff (X \ Y) = X

    proof

      thus X misses Y implies (X \ Y) = X

      proof

        assume

         A1: (X /\ Y) = {} ;

        thus for x be object holds x in (X \ Y) implies x in X by XBOOLE_0:def 5;

        let x be object;

         not x in (X /\ Y) implies not x in X or not x in Y by XBOOLE_0:def 4;

        hence thesis by A1, XBOOLE_0:def 5;

      end;

      assume

       A2: (X \ Y) = X;

       not ex x be object st x in (X /\ Y)

      proof

        given x be object such that

         A3: x in (X /\ Y);

        x in X & x in Y by A3, XBOOLE_0:def 4;

        hence contradiction by A2, XBOOLE_0:def 5;

      end;

      hence thesis by XBOOLE_0: 4;

    end;

    theorem :: XBOOLE_1:84

    X meets Y & X misses Z implies X meets (Y \ Z)

    proof

      assume that

       A1: X meets Y and

       A2: X misses Z;

      (X /\ (Y \ Z)) = ((X /\ Y) \ (X /\ Z)) by Th50

      .= ((X /\ Y) \ {} ) by A2;

      hence (X /\ (Y \ Z)) <> {} by A1;

    end;

    theorem :: XBOOLE_1:85

    X c= Y implies X misses (Z \ Y)

    proof

      assume

       A1: X c= Y;



      thus (X /\ (Z \ Y)) = ((Z /\ X) \ Y) by Th49

      .= (Z /\ (X \ Y)) by Th49

      .= (Z /\ {} ) by A1, Lm1

      .= {} ;

    end;

    theorem :: XBOOLE_1:86



     Th86: X c= Y & X misses Z implies X c= (Y \ Z)

    proof

      assume

       A1: X c= Y & (X /\ Z) = {} ;

      let x be object;

      assume x in X;

      then x in Y & not x in Z by A1, XBOOLE_0:def 4;

      hence thesis by XBOOLE_0:def 5;

    end;

    theorem :: XBOOLE_1:87

    Y misses Z implies ((X \ Y) \/ Z) = ((X \/ Z) \ Y)

    proof

      assume

       A1: Y misses Z;



      thus ((X \/ Z) \ Y) = ((X \ Y) \/ (Z \ Y)) by Th42

      .= ((X \ Y) \/ Z) by A1, Th83;

    end;

    theorem :: XBOOLE_1:88



     Th88: X misses Y implies ((X \/ Y) \ Y) = X

    proof

      assume

       A1: X misses Y;



      thus ((X \/ Y) \ Y) = ((X \ Y) \/ (Y \ Y)) by Th42

      .= ((X \ Y) \/ {} ) by Lm1

      .= X by A1, Th83;

    end;

    theorem :: XBOOLE_1:89



     Th89: (X /\ Y) misses (X \ Y)

    proof

      now

        let x be object;

         not (x in X & x in Y & not x in Y);

        hence not (x in (X /\ Y) & x in (X \ Y)) by XBOOLE_0:def 4, XBOOLE_0:def 5;

      end;

      hence thesis by XBOOLE_0: 3;

    end;

    theorem :: XBOOLE_1:90

    (X \ (X /\ Y)) misses Y

    proof

      (X \ (X /\ Y)) = (X \ Y) by Th47;

      hence thesis by Th79;

    end;

    theorem :: XBOOLE_1:91

    ((X \+\ Y) \+\ Z) = (X \+\ (Y \+\ Z))

    proof

      set S1 = (X \ (Y \/ Z)), S2 = (Y \ (X \/ Z)), S3 = (Z \ (X \/ Y)), S4 = ((X /\ Y) /\ Z);



      thus ((X \+\ Y) \+\ Z) = ((((X \ Y) \ Z) \/ ((Y \ X) \ Z)) \/ (Z \ ((X \ Y) \/ (Y \ X)))) by Th42

      .= ((S1 \/ ((Y \ X) \ Z)) \/ (Z \ ((X \ Y) \/ (Y \ X)))) by Th41

      .= ((S1 \/ S2) \/ (Z \ ((X \ Y) \/ (Y \ X)))) by Th41

      .= ((S1 \/ S2) \/ (Z \ ((X \/ Y) \ (X /\ Y)))) by Th55

      .= ((S1 \/ S2) \/ (S4 \/ S3)) by Th52

      .= (((S1 \/ S2) \/ S4) \/ S3) by Th4

      .= (((S1 \/ S4) \/ S2) \/ S3) by Th4

      .= ((S1 \/ S4) \/ (S2 \/ S3)) by Th4

      .= ((S1 \/ (X /\ (Y /\ Z))) \/ (S2 \/ S3)) by Th16

      .= ((X \ ((Y \/ Z) \ (Y /\ Z))) \/ (S2 \/ S3)) by Th52

      .= ((X \ ((Y \ Z) \/ (Z \ Y))) \/ (S2 \/ (Z \ (Y \/ X)))) by Th55

      .= ((X \ ((Y \ Z) \/ (Z \ Y))) \/ ((Y \ (Z \/ X)) \/ ((Z \ Y) \ X))) by Th41

      .= ((X \ ((Y \ Z) \/ (Z \ Y))) \/ (((Y \ Z) \ X) \/ ((Z \ Y) \ X))) by Th41

      .= (X \+\ (Y \+\ Z)) by Th42;

    end;

    theorem :: XBOOLE_1:92

    (X \+\ X) = {} by Lm1;

    theorem :: XBOOLE_1:93



     Th93: (X \/ Y) = ((X \+\ Y) \/ (X /\ Y))

    proof



      thus (X \/ Y) = (((X \ Y) \/ (X /\ Y)) \/ Y) by Th51

      .= ((X \ Y) \/ ((X /\ Y) \/ Y)) by Th4

      .= ((X \ Y) \/ Y) by Th22

      .= ((X \ Y) \/ ((Y \ X) \/ (Y /\ X))) by Th51

      .= ((X \+\ Y) \/ (X /\ Y)) by Th4;

    end;



     Lm4: (X /\ Y) misses (X \+\ Y)

    proof

      (X /\ Y) misses (X \ Y) & (X /\ Y) misses (Y \ X) by Th89;

      hence thesis by Th70;

    end;



     Lm5: (X \+\ Y) = ((X \/ Y) \ (X /\ Y))

    proof



      thus (X \+\ Y) = ((X \ (X /\ Y)) \/ (Y \ X)) by Th47

      .= ((X \ (X /\ Y)) \/ (Y \ (X /\ Y))) by Th47

      .= ((X \/ Y) \ (X /\ Y)) by Th42;

    end;

    theorem :: XBOOLE_1:94

    (X \/ Y) = ((X \+\ Y) \+\ (X /\ Y))

    proof

      (X /\ Y) misses (X \+\ Y) by Lm4;

      then ((X \+\ Y) \ (X /\ Y)) = (X \+\ Y) & ((X /\ Y) \ (X \+\ Y)) = (X /\ Y) by Th83;

      hence thesis by Th93;

    end;

    theorem :: XBOOLE_1:95

    (X /\ Y) = ((X \+\ Y) \+\ (X \/ Y))

    proof

      (X \+\ Y) = ((X \/ Y) \ (X /\ Y)) by Lm5;

      then (X \+\ Y) c= (X \/ Y) by Th36;

      then

       A1: ((X \+\ Y) \ (X \/ Y)) = {} by Lm1;

      (X \/ Y) = ((X \+\ Y) \/ (X /\ Y)) by Th93;

      hence thesis by A1, Lm4, Th88;

    end;

    theorem :: XBOOLE_1:96

    (X \ Y) c= (X \+\ Y) by Th7;

    theorem :: XBOOLE_1:97

    (X \ Y) c= Z & (Y \ X) c= Z implies (X \+\ Y) c= Z by Th8;

    theorem :: XBOOLE_1:98

    (X \/ Y) = (X \+\ (Y \ X))

    proof



       A1: ((Y \ X) \ X) = (Y \ (X \/ X)) by Th41

      .= (Y \ X);

      (X \ (Y \ X)) = ((X \ Y) \/ (X /\ X)) by Th52

      .= X by Th12, Th36;

      hence thesis by A1, Th39;

    end;

    theorem :: XBOOLE_1:99

    ((X \+\ Y) \ Z) = ((X \ (Y \/ Z)) \/ (Y \ (X \/ Z)))

    proof



      thus ((X \+\ Y) \ Z) = (((X \ Y) \ Z) \/ ((Y \ X) \ Z)) by Th42

      .= ((X \ (Y \/ Z)) \/ ((Y \ X) \ Z)) by Th41

      .= ((X \ (Y \/ Z)) \/ (Y \ (X \/ Z))) by Th41;

    end;

    theorem :: XBOOLE_1:100

    (X \ Y) = (X \+\ (X /\ Y))

    proof

      (X /\ Y) c= X by Th17;

      then ((X /\ Y) \ X) = {} by Lm1;

      hence thesis by Th47;

    end;

    theorem :: XBOOLE_1:101

    (X \+\ Y) = ((X \/ Y) \ (X /\ Y)) by Lm5;

    theorem :: XBOOLE_1:102

    (X \ (Y \+\ Z)) = ((X \ (Y \/ Z)) \/ ((X /\ Y) /\ Z))

    proof



      thus (X \ (Y \+\ Z)) = (X \ ((Y \/ Z) \ (Y /\ Z))) by Lm5

      .= ((X \ (Y \/ Z)) \/ (X /\ (Y /\ Z))) by Th52

      .= ((X \ (Y \/ Z)) \/ ((X /\ Y) /\ Z)) by Th16;

    end;

    theorem :: XBOOLE_1:103

    (X /\ Y) misses (X \+\ Y) by Lm4;

    theorem :: XBOOLE_1:104

    X c< Y or X = Y or Y c< X iff (X,Y) are_c=-comparable ;

    begin

    theorem :: XBOOLE_1:105

    for X,Y be set st X c< Y holds (Y \ X) <> {} by Th60, Lm1;

    theorem :: XBOOLE_1:106



     Th106: X c= (A \ B) implies X c= A & X misses B

    proof

      assume

       A1: X c= (A \ B);

      (A \ B) c= A by Th36;

      hence X c= A by A1;

      now

        let x be object;

        assume x in X;

        then x in (A \ B) by A1;

        hence not x in B by XBOOLE_0:def 5;

      end;

      hence thesis by XBOOLE_0: 3;

    end;

    theorem :: XBOOLE_1:107

    X c= (A \+\ B) iff X c= (A \/ B) & X misses (A /\ B)

    proof

      (A \+\ B) = ((A \/ B) \ (A /\ B)) by Lm5;

      hence thesis by Th86, Th106;

    end;

    theorem :: XBOOLE_1:108

    X c= A implies (X /\ Y) c= A

    proof

      (X /\ Y) c= X by Th17;

      hence thesis;

    end;

    theorem :: XBOOLE_1:109



     Th109: X c= A implies (X \ Y) c= A

    proof

      (X \ Y) c= X by Th36;

      hence thesis;

    end;

    theorem :: XBOOLE_1:110

    X c= A & Y c= A implies (X \+\ Y) c= A

    proof

      assume X c= A & Y c= A;

      then (X \ Y) c= A & (Y \ X) c= A by Th109;

      hence thesis by Th8;

    end;

    theorem :: XBOOLE_1:111



     Th111: ((X /\ Z) \ (Y /\ Z)) = ((X \ Y) /\ Z)

    proof



      thus ((X /\ Z) \ (Y /\ Z)) = (((X /\ Z) \ Y) \/ ((X /\ Z) \ Z)) by Lm2

      .= (((X /\ Z) \ Y) \/ (X /\ (Z \ Z))) by Th49

      .= (((X /\ Z) \ Y) \/ (X /\ {} )) by Lm1

      .= ((X \ Y) /\ Z) by Th49;

    end;

    theorem :: XBOOLE_1:112

    ((X /\ Z) \+\ (Y /\ Z)) = ((X \+\ Y) /\ Z)

    proof



      thus ((X /\ Z) \+\ (Y /\ Z)) = (((X \ Y) /\ Z) \/ ((Y /\ Z) \ (X /\ Z))) by Th111

      .= (((X \ Y) /\ Z) \/ ((Y \ X) /\ Z)) by Th111

      .= ((X \+\ Y) /\ Z) by Th23;

    end;

    theorem :: XBOOLE_1:113

    (((X \/ Y) \/ Z) \/ V) = (X \/ ((Y \/ Z) \/ V))

    proof

      (((X \/ Y) \/ Z) \/ V) = ((X \/ Y) \/ (Z \/ V)) by Th4

      .= (X \/ (Y \/ (Z \/ V))) by Th4

      .= (X \/ ((Y \/ Z) \/ V)) by Th4;

      hence thesis;

    end;

    theorem :: XBOOLE_1:114

    for A,B,C,D be set st A misses D & B misses D & C misses D holds ((A \/ B) \/ C) misses D

    proof

      let A,B,C,D be set;

      assume A misses D & B misses D;

      then

       A1: (A \/ B) misses D by Th70;

      assume C misses D;

      hence thesis by A1, Th70;

    end;

    ::$Canceled

    theorem :: XBOOLE_1:116

    (X /\ (Y /\ Z)) = ((X /\ Y) /\ (X /\ Z))

    proof



      thus (X /\ (Y /\ Z)) = (((X /\ X) /\ Y) /\ Z) by Th16

      .= ((X /\ (X /\ Y)) /\ Z) by Th16

      .= ((X /\ Y) /\ (X /\ Z)) by Th16;

    end;

    theorem :: XBOOLE_1:117

    for P,G,C be set st C c= G holds (P \ C) = ((P \ G) \/ (P /\ (G \ C)))

    proof

      let P,G,C be set;

      assume C c= G;

      then

       A1: (P \ G) c= (P \ C) by Th34;

      thus (P \ C) c= ((P \ G) \/ (P /\ (G \ C)))

      proof

        let x be object;

        assume x in (P \ C);

        then x in P & not x in G or x in P & x in G & not x in C by XBOOLE_0:def 5;

        then x in (P \ G) or x in P & x in (G \ C) by XBOOLE_0:def 5;

        then x in (P \ G) or x in (P /\ (G \ C)) by XBOOLE_0:def 4;

        hence thesis by XBOOLE_0:def 3;

      end;

      (P /\ (G \ C)) = ((P /\ G) \ C) & ((P /\ G) \ C) c= (P \ C) by Th17, Th33, Th49;

      hence thesis by A1, Th8;

    end;