interva1.miz



    begin

    definition

      let U be set;

      let X,Y be Subset of U;

      :: INTERVA1:def1

      func Inter (X,Y) -> Subset-Family of U equals { A where A be Subset of U : X c= A & A c= Y };

      coherence

      proof

        set IT = { A where A be Subset of U : X c= A & A c= Y };

        IT c= ( bool U)

        proof

          let x be object;

          assume x in IT;

          then x in { A where A be Subset of U : X c= A & A c= Y };

          then

          consider B be Subset of U such that

           A1: x = B & X c= B & B c= Y;

          thus thesis by A1;

        end;

        then IT is Subset-Family of U;

        hence thesis;

      end;

    end

    reserve U for set,

X,Y for Subset of U;

    theorem :: INTERVA1:1

    

     Th1: for x be set holds x in ( Inter (X,Y)) iff X c= x & x c= Y

    proof

      let x be set;

      hereby

        assume x in ( Inter (X,Y));

        then

        consider A9 be Element of ( bool U) such that

         A1: x = A9 & X c= A9 & A9 c= Y;

        thus X c= x & x c= Y by A1;

      end;

      assume

       A2: X c= x & x c= Y;

      then x is Subset of U by XBOOLE_1: 1;

      hence thesis by A2;

    end;

    theorem :: INTERVA1:2

    

     Th2: ( Inter (X,Y)) <> {} implies X in ( Inter (X,Y)) & Y in ( Inter (X,Y))

    proof

      assume ( Inter (X,Y)) <> {} ;

      then

      consider x be object such that

       A1: x in ( Inter (X,Y)) by XBOOLE_0:def 1;

      reconsider x as set by TARSKI: 1;

      X c= x & x c= Y by A1, Th1;

      then X c= Y;

      hence thesis;

    end;

    theorem :: INTERVA1:3

    

     Th3: for U be set, A,B be Subset of U st not A c= B holds ( Inter (A,B)) = {}

    proof

      let U be set, A,B be Subset of U;

      assume

       A1: not A c= B;

      assume ( Inter (A,B)) <> {} ;

      then

      consider x be object such that

       A2: x in ( Inter (A,B)) by XBOOLE_0:def 1;

      reconsider x as set by TARSKI: 1;

      A c= x & x c= B by A2, Th1;

      hence thesis by A1;

    end;

    theorem :: INTERVA1:4

    for U be set, A,B be Subset of U st ( Inter (A,B)) = {} holds not A c= B by Th1;

    theorem :: INTERVA1:5

    

     Th5: for A,B be Subset of U st ( Inter (A,B)) <> {} holds A c= B

    proof

      let A,B be Subset of U;

      assume ( Inter (A,B)) <> {} ;

      then

      consider x be object such that

       A1: x in ( Inter (A,B)) by XBOOLE_0:def 1;

      reconsider x as set by TARSKI: 1;

      A c= x & x c= B by A1, Th1;

      hence thesis;

    end;

    theorem :: INTERVA1:6

    

     Th6: for A,B,C,D be Subset of U st ( Inter (A,B)) <> {} & ( Inter (A,B)) = ( Inter (C,D)) holds A = C & B = D

    proof

      let A,B,C,D be Subset of U;

      assume

       A1: ( Inter (A,B)) <> {} & ( Inter (A,B)) = ( Inter (C,D));

      then A in ( Inter (A,B)) by Th2;

      then

       A2: C c= A & A c= D by Th1, A1;

      C in ( Inter (C,D)) by A1, Th2;

      then

       A3: A c= C & C c= B by A1, Th1;

      B in ( Inter (A,B)) by A1, Th2;

      then

       A4: B c= D by Th1, A1;

      D in ( Inter (C,D)) by A1, Th2;

      then D c= B by A1, Th1;

      hence thesis by A3, A4, A2;

    end;

    theorem :: INTERVA1:7

    

     Th7: for U be non empty set, A be non empty Subset of U holds ( Inter (A,( {} U))) = {}

    proof

      let U be non empty set, A be non empty Subset of U;

      thus ( Inter (A,( {} U))) c= {}

      proof

        let x be object;

        reconsider xx = x as set by TARSKI: 1;

        assume x in ( Inter (A,( {} U)));

        then A c= xx & xx c= ( {} U) by Th1;

        hence thesis;

      end;

      thus thesis;

    end;

    theorem :: INTERVA1:8

    

     Th8: for A be Subset of U holds ( Inter (A,A)) = {A}

    proof

      let A be Subset of U;

      thus ( Inter (A,A)) c= {A}

      proof

        let x be object;

        reconsider xx = x as set by TARSKI: 1;

        assume x in ( Inter (A,A));

        then A c= xx & xx c= A by Th1;

        then A = x by XBOOLE_0:def 10;

        hence thesis by TARSKI:def 1;

      end;

      let x be object;

      assume x in {A};

      then x = A by TARSKI:def 1;

      hence thesis;

    end;

    definition

      let U;

      :: INTERVA1:def2

      mode IntervalSet of U -> Subset-Family of U means

      : Def2: ex A,B be Subset of U st it = ( Inter (A,B));

      existence

      proof

        set A = the Subset of U;

        set IT = {A};

        IT = ( Inter (A,A)) by Th8;

        hence thesis;

      end;

    end

    theorem :: INTERVA1:9

    for U be non empty set holds {} is IntervalSet of U

    proof

      let U be non empty set;

      set A = the non empty Subset of U;

      ( Inter (A,( {} U))) = {} by Th7;

      hence thesis by Def2;

    end;

    theorem :: INTERVA1:10

    

     Th10: for U be non empty set, A be Subset of U holds {A} is IntervalSet of U

    proof

      let U be non empty set, A be Subset of U;

      ( Inter (A,A)) = {A} by Th8;

      hence thesis by Def2;

    end;

    definition

      let U;

      let A,B be Subset of U;

      :: original: Inter

      redefine

      func Inter (A,B) -> IntervalSet of U ;

      correctness by Def2;

    end

    registration

      let U be non empty set;

      cluster non empty for IntervalSet of U;

      existence

      proof

        set A = the Subset of U;

         {A} is IntervalSet of U by Th10;

        hence thesis;

      end;

    end

    theorem :: INTERVA1:11

    

     Th11: for U be non empty set, A be set holds A is non empty IntervalSet of U iff ex A1,A2 be Subset of U st A1 c= A2 & A = ( Inter (A1,A2))

    proof

      let U be non empty set, A be set;

      hereby

        assume

         A1: A is non empty IntervalSet of U;

        then

        consider A1,A2 be Subset of U such that

         A2: A = ( Inter (A1,A2)) by Def2;

        take A1, A2;

        thus A1 c= A2 by A1, A2, Th3;

        thus A = ( Inter (A1,A2)) by A2;

      end;

      given A1,A2 be Subset of U such that

       A3: A1 c= A2 & A = ( Inter (A1,A2));

      A1 in ( Inter (A1,A2)) by A3;

      hence thesis by A3;

    end;

    theorem :: INTERVA1:12

    

     Th12: for U be non empty set, A1,A2,B1,B2 be Subset of U st A1 c= A2 & B1 c= B2 holds ( INTERSECTION (( Inter (A1,A2)),( Inter (B1,B2)))) = { C where C be Subset of U : (A1 /\ B1) c= C & C c= (A2 /\ B2) }

    proof

      let U be non empty set, A1,A2,B1,B2 be Subset of U;

      assume that

       A1: A1 c= A2 and

       A2: B1 c= B2;

      set A = ( Inter (A1,A2)), B = ( Inter (B1,B2));

      set LAB = (A1 /\ B1);

      set UAB = (A2 /\ B2);

      set IT = ( INTERSECTION (( Inter (A1,A2)),( Inter (B1,B2))));

      thus IT c= { C where C be Subset of U : LAB c= C & C c= UAB }

      proof

        let x be object;

        reconsider xx = x as set by TARSKI: 1;

        assume x in IT;

        then

        consider X,Y be set such that

         A3: X in A & Y in B & x = (X /\ Y) by SETFAM_1:def 5;

        xx c= X by A3, XBOOLE_1: 17;

        then

         A4: x is Subset of U by A3, XBOOLE_1: 1;

        

         A5: A1 c= X by Th1, A3;

        B1 c= Y by Th1, A3;

        then

         A6: LAB c= xx by A5, A3, XBOOLE_1: 27;

        

         A7: X c= A2 by Th1, A3;

        Y c= B2 by Th1, A3;

        then xx c= UAB by A7, A3, XBOOLE_1: 27;

        hence thesis by A6, A4;

      end;

      let x be object;

      reconsider xx = x as set by TARSKI: 1;

      assume x in { C where C be Subset of U : LAB c= C & C c= UAB };

      then

      consider C9 be Subset of U such that

       A8: C9 = x & LAB c= C9 & C9 c= UAB;

      set x1 = ((xx \/ A1) /\ A2);

      set x2 = ((xx \/ B1) /\ B2);

      

       A9: (LAB \/ xx) = x by A8, XBOOLE_1: 12;

      

       A10: (UAB /\ xx) = x by A8, XBOOLE_1: 28;

      

       A11: (x1 /\ x2) = ((xx \/ A1) /\ (A2 /\ ((xx \/ B1) /\ B2))) by XBOOLE_1: 16

      .= ((xx \/ A1) /\ ((xx \/ B1) /\ (B2 /\ A2))) by XBOOLE_1: 16

      .= (((xx \/ A1) /\ (xx \/ B1)) /\ UAB) by XBOOLE_1: 16

      .= x by A9, A10, XBOOLE_1: 24;

      (A1 /\ A2) = A1 by A1, XBOOLE_1: 28;

      then x1 = ((xx /\ A2) \/ A1) by XBOOLE_1: 23;

      then

       A12: A1 c= x1 by XBOOLE_1: 7;

      x1 c= A2 by XBOOLE_1: 17;

      then

       A13: x1 in A by A12;

      (B1 /\ B2) = B1 by A2, XBOOLE_1: 28;

      then x2 = ((xx /\ B2) \/ B1) by XBOOLE_1: 23;

      then

       A14: B1 c= x2 by XBOOLE_1: 7;

      x2 c= B2 by XBOOLE_1: 17;

      then x2 in B by A14;

      hence thesis by A11, A13, SETFAM_1:def 5;

    end;

    theorem :: INTERVA1:13

    

     Th13: for U be non empty set, A1,A2,B1,B2 be Subset of U st A1 c= A2 & B1 c= B2 holds ( UNION (( Inter (A1,A2)),( Inter (B1,B2)))) = { C where C be Subset of U : (A1 \/ B1) c= C & C c= (A2 \/ B2) }

    proof

      let U be non empty set, A1,A2,B1,B2 be Subset of U;

      assume that

       A1: A1 c= A2 and

       A2: B1 c= B2;

      set A = ( Inter (A1,A2)), B = ( Inter (B1,B2));

      set LAB = (A1 \/ B1);

      set UAB = (A2 \/ B2);

      set IT = ( UNION (A,B));

      thus IT c= { C where C be Subset of U : LAB c= C & C c= UAB }

      proof

        let x be object;

        reconsider xx = x as set by TARSKI: 1;

        assume x in IT;

        then

        consider X,Y be set such that

         A3: X in A & Y in B & x = (X \/ Y) by SETFAM_1:def 4;

        

         A4: x is Subset of U by A3, XBOOLE_1: 8;

        

         A5: A1 c= X by Th1, A3;

        B1 c= Y by Th1, A3;

        then

         A6: LAB c= xx by A5, A3, XBOOLE_1: 13;

        

         A7: X c= A2 by Th1, A3;

        Y c= B2 by Th1, A3;

        then xx c= UAB by A7, A3, XBOOLE_1: 13;

        hence thesis by A4, A6;

      end;

      let x be object;

      reconsider xx = x as set by TARSKI: 1;

      assume x in { C where C be Subset of U : LAB c= C & C c= UAB };

      then

      consider C9 be Subset of U such that

       A8: C9 = x & LAB c= C9 & C9 c= UAB;

      set x1 = ((xx \/ A1) /\ A2);

      set x2 = ((xx \/ B1) /\ B2);

      

       A9: (LAB \/ xx) = x by A8, XBOOLE_1: 12;

      

       A10: (UAB /\ xx) = x by A8, XBOOLE_1: 28;

      

       A11: (A1 /\ A2) = A1 by A1, XBOOLE_1: 28;

      

       A12: (B1 /\ B2) = B1 by A2, XBOOLE_1: 28;

      

       A13: (x1 \/ x2) = (((xx /\ A2) \/ (A1 /\ A2)) \/ ((xx \/ B1) /\ B2)) by XBOOLE_1: 23

      .= (((xx /\ A2) \/ A1) \/ ((xx /\ B2) \/ (B1 /\ B2))) by A11, XBOOLE_1: 23

      .= ((xx /\ A2) \/ (A1 \/ ((xx /\ B2) \/ B1))) by A12, XBOOLE_1: 4

      .= ((xx /\ A2) \/ ((xx /\ B2) \/ LAB)) by XBOOLE_1: 4

      .= (((xx /\ A2) \/ (xx /\ B2)) \/ LAB) by XBOOLE_1: 4

      .= x by A9, A10, XBOOLE_1: 23;

      (A1 /\ A2) = A1 by A1, XBOOLE_1: 28;

      then x1 = ((xx /\ A2) \/ A1) by XBOOLE_1: 23;

      then

       A14: A1 c= x1 by XBOOLE_1: 7;

      x1 c= A2 by XBOOLE_1: 17;

      then

       A15: x1 in A by A14;

      (B1 /\ B2) = B1 by A2, XBOOLE_1: 28;

      then x2 = ((xx /\ B2) \/ B1) by XBOOLE_1: 23;

      then

       A16: B1 c= x2 by XBOOLE_1: 7;

      x2 c= B2 by XBOOLE_1: 17;

      then x2 in B by A16;

      hence thesis by A13, A15, SETFAM_1:def 4;

    end;

    definition

      let U be non empty set, A,B be non empty IntervalSet of U;

      :: INTERVA1:def3

      func A _/\_ B -> IntervalSet of U equals ( INTERSECTION (A,B));

      coherence

      proof

        set IT = ( INTERSECTION (A,B));

        consider A1,A2 be Subset of U such that

         A1: A1 c= A2 & A = ( Inter (A1,A2)) by Th11;

        consider B1,B2 be Subset of U such that

         A2: B1 c= B2 & B = ( Inter (B1,B2)) by Th11;

        set LAB = (A1 /\ B1);

        set UAB = (A2 /\ B2);

        IT = ( Inter (LAB,UAB)) by Th12, A1, A2;

        hence thesis;

      end;

      :: INTERVA1:def4

      func A _\/_ B -> IntervalSet of U equals ( UNION (A,B));

      coherence

      proof

        set IT = ( UNION (A,B));

        consider A1,A2 be Subset of U such that

         A3: A1 c= A2 & A = ( Inter (A1,A2)) by Th11;

        consider B1,B2 be Subset of U such that

         A4: B1 c= B2 & B = ( Inter (B1,B2)) by Th11;

        set LAB = (A1 \/ B1);

        set UAB = (A2 \/ B2);

        IT = ( Inter (LAB,UAB)) by Th13, A3, A4;

        hence thesis;

      end;

    end

    registration

      let U be non empty set, A,B be non empty IntervalSet of U;

      cluster (A _/\_ B) -> non empty;

      coherence by TOPGEN_4: 31;

      cluster (A _\/_ B) -> non empty;

      coherence by TOPGEN_4: 30;

    end

    reserve U for non empty set,

A,B,C for non empty IntervalSet of U;

    definition

      let U, A;

      :: INTERVA1:def5

      func A ``1 -> Subset of U means

      : Def5: ex B be Subset of U st A = ( Inter (it ,B));

      existence

      proof

        consider A1,A2 be Subset of U such that

         A1: A1 c= A2 & A = ( Inter (A1,A2)) by Th11;

        thus thesis by A1;

      end;

      uniqueness by Th6;

      :: INTERVA1:def6

      func A ``2 -> Subset of U means

      : Def6: ex B be Subset of U st A = ( Inter (B,it ));

      existence

      proof

        consider A1,A2 be Subset of U such that

         A2: A1 c= A2 & A = ( Inter (A1,A2)) by Th11;

        thus thesis by A2;

      end;

      uniqueness by Th6;

    end

    theorem :: INTERVA1:14

    

     Th14: for X be set holds X in A iff (A ``1 ) c= X & X c= (A ``2 )

    proof

      let X be set;

      

       A1: X in A implies (A ``1 ) c= X & X c= (A ``2 )

      proof

        assume

         A2: X in A;

        

         A3: (A ``1 ) c= X

        proof

          consider B be Subset of U such that

           A4: A = ( Inter ((A ``1 ),B)) by Def5;

          thus thesis by Th1, A2, A4;

        end;

        X c= (A ``2 )

        proof

          consider B be Subset of U such that

           A5: A = ( Inter (B,(A ``2 ))) by Def6;

          thus thesis by Th1, A2, A5;

        end;

        hence thesis by A3;

      end;

      (A ``1 ) c= X & X c= (A ``2 ) implies X in A

      proof

        assume (A ``1 ) c= X & X c= (A ``2 );

        then

         A6: X in ( Inter ((A ``1 ),(A ``2 ))) by Th1;

        consider B be Subset of U such that

         A7: A = ( Inter ((A ``1 ),B)) by Def5;

        consider C be Subset of U such that

         A8: A = ( Inter (C,(A ``2 ))) by Def6;

        thus thesis by A7, A6, Th6, A8;

      end;

      hence thesis by A1;

    end;

    theorem :: INTERVA1:15

    

     Th15: A = ( Inter ((A ``1 ),(A ``2 )))

    proof

      

       A1: ( Inter ((A ``1 ),(A ``2 ))) c= A

      proof

        let x be object;

        reconsider xx = x as set by TARSKI: 1;

        assume x in ( Inter ((A ``1 ),(A ``2 )));

        then (A ``1 ) c= xx & xx c= (A ``2 ) by Th1;

        hence thesis by Th14;

      end;

      A c= ( Inter ((A ``1 ),(A ``2 )))

      proof

        let x be object;

        reconsider xx = x as set by TARSKI: 1;

        assume x in A;

        then (A ``1 ) c= xx & xx c= (A ``2 ) by Th14;

        hence thesis by Th1;

      end;

      hence thesis by A1;

    end;

    theorem :: INTERVA1:16

    

     Th16: (A ``1 ) c= (A ``2 )

    proof

      consider B be Subset of U such that

       A1: A = ( Inter ((A ``1 ),B)) by Def5;

      consider C be Subset of U such that

       A2: A = ( Inter (C,(A ``2 ))) by Def6;

      (A ``1 ) = C by Th6, A2, A1;

      hence thesis by Th5, A2;

    end;

    theorem :: INTERVA1:17

    

     Th17: (A _\/_ B) = ( Inter (((A ``1 ) \/ (B ``1 )),((A ``2 ) \/ (B ``2 ))))

    proof

      thus (A _\/_ B) c= ( Inter (((A ``1 ) \/ (B ``1 )),((A ``2 ) \/ (B ``2 ))))

      proof

        let x be object;

        reconsider xx = x as set by TARSKI: 1;

        assume

         A1: x in (A _\/_ B);

        then

        consider X,Y be set such that

         A2: X in A & Y in B & x = (X \/ Y) by SETFAM_1:def 4;

        

         A3: (A ``1 ) c= X & X c= (A ``2 ) by A2, Th14;

        

         A4: (B ``1 ) c= Y & Y c= (B ``2 ) by A2, Th14;

        then

         A5: xx c= ((A ``2 ) \/ (B ``2 )) by A3, A2, XBOOLE_1: 13;

        ((A ``1 ) \/ (B ``1 )) c= xx by A3, A2, A4, XBOOLE_1: 13;

        hence thesis by A1, A5;

      end;

      thus ( Inter (((A ``1 ) \/ (B ``1 )),((A ``2 ) \/ (B ``2 )))) c= (A _\/_ B)

      proof

        let x be object;

        assume x in ( Inter (((A ``1 ) \/ (B ``1 )),((A ``2 ) \/ (B ``2 ))));

        then

        consider Z be Element of ( bool U) such that

         A6: x = Z & ((A ``1 ) \/ (B ``1 )) c= Z & Z c= ((A ``2 ) \/ (B ``2 ));

        (A ``1 ) c= ((Z \/ (A ``1 )) /\ (A ``2 ))

        proof

          let x be object;

          assume

           A7: x in (A ``1 );

          assume

           A8: not x in ((Z \/ (A ``1 )) /\ (A ``2 ));

          per cases by A8, XBOOLE_0:def 4;

            suppose not x in (Z \/ (A ``1 ));

            hence thesis by A7, XBOOLE_0:def 3;

          end;

            suppose

             A9: not x in (A ``2 );

            (A ``1 ) c= (A ``2 ) & x in (A ``1 ) by A7, Th16;

            hence thesis by A9;

          end;

        end;

        then (A ``1 ) c= ((Z \/ (A ``1 )) /\ (A ``2 )) & ((Z \/ (A ``1 )) /\ (A ``2 )) c= (A ``2 ) by XBOOLE_1: 17;

        then

         A10: ((Z \/ (A ``1 )) /\ (A ``2 )) in A by Th14;

        (B ``1 ) c= ((Z \/ (B ``1 )) /\ (B ``2 ))

        proof

          let x be object;

          assume

           A11: x in (B ``1 );

          then

           A12: x in (Z \/ (B ``1 )) by XBOOLE_0:def 3;

          (B ``1 ) c= (B ``2 ) by Th16;

          hence thesis by A11, A12, XBOOLE_0:def 4;

        end;

        then (B ``1 ) c= ((Z \/ (B ``1 )) /\ (B ``2 )) & ((Z \/ (B ``1 )) /\ (B ``2 )) c= (B ``2 ) by XBOOLE_1: 17;

        then

         A13: ((Z \/ (B ``1 )) /\ (B ``2 )) in B by Th14;

        (((Z \/ (A ``1 )) /\ (A ``2 )) \/ ((Z \/ (B ``1 )) /\ (B ``2 ))) = ((((Z \/ (A ``1 )) /\ (A ``2 )) \/ (Z \/ (B ``1 ))) /\ (((Z \/ (A ``1 )) /\ (A ``2 )) \/ (B ``2 ))) by XBOOLE_1: 24

        .= ((((Z \/ (A ``1 )) \/ (Z \/ (B ``1 ))) /\ ((A ``2 ) \/ (Z \/ (B ``1 )))) /\ (((Z \/ (A ``1 )) /\ (A ``2 )) \/ (B ``2 ))) by XBOOLE_1: 24

        .= (((Z \/ ((A ``1 ) \/ (B ``1 ))) /\ ((A ``2 ) \/ (Z \/ (B ``1 )))) /\ (((Z \/ (A ``1 )) /\ (A ``2 )) \/ (B ``2 ))) by XBOOLE_1: 5

        .= ((Z /\ ((A ``2 ) \/ (Z \/ (B ``1 )))) /\ (((Z \/ (A ``1 )) /\ (A ``2 )) \/ (B ``2 ))) by A6, XBOOLE_1: 12

        .= (((Z /\ (A ``2 )) \/ (Z /\ (Z \/ (B ``1 )))) /\ (((Z \/ (A ``1 )) /\ (A ``2 )) \/ (B ``2 ))) by XBOOLE_1: 23

        .= (((Z /\ (A ``2 )) \/ Z) /\ (((Z \/ (A ``1 )) /\ (A ``2 )) \/ (B ``2 ))) by XBOOLE_1: 7, XBOOLE_1: 28

        .= (Z /\ ((B ``2 ) \/ ((Z \/ (A ``1 )) /\ (A ``2 )))) by XBOOLE_1: 12, XBOOLE_1: 17

        .= (Z /\ (((Z \/ (A ``1 )) \/ (B ``2 )) /\ ((A ``2 ) \/ (B ``2 )))) by XBOOLE_1: 24

        .= (Z /\ ((Z \/ ((A ``1 ) \/ (B ``2 ))) /\ ((A ``2 ) \/ (B ``2 )))) by XBOOLE_1: 4

        .= (Z /\ ((Z /\ ((A ``2 ) \/ (B ``2 ))) \/ (((A ``1 ) \/ (B ``2 )) /\ ((A ``2 ) \/ (B ``2 ))))) by XBOOLE_1: 23

        .= (Z /\ (Z \/ (((A ``1 ) \/ (B ``2 )) /\ ((A ``2 ) \/ (B ``2 ))))) by A6, XBOOLE_1: 28

        .= (Z /\ ((Z \/ ((A ``1 ) \/ (B ``2 ))) /\ (Z \/ ((A ``2 ) \/ (B ``2 ))))) by XBOOLE_1: 24

        .= ((Z /\ (Z \/ ((A ``1 ) \/ (B ``2 )))) /\ (Z \/ ((A ``2 ) \/ (B ``2 )))) by XBOOLE_1: 16

        .= (Z /\ (Z \/ ((A ``2 ) \/ (B ``2 )))) by XBOOLE_1: 7, XBOOLE_1: 28

        .= Z by XBOOLE_1: 7, XBOOLE_1: 28;

        then

        consider X,Y be Subset of U such that

         A14: X in A & Y in B & Z = (X \/ Y) by A10, A13;

        thus thesis by A14, A6, SETFAM_1:def 4;

      end;

    end;

    theorem :: INTERVA1:18

    

     Th18: (A _/\_ B) = ( Inter (((A ``1 ) /\ (B ``1 )),((A ``2 ) /\ (B ``2 ))))

    proof

      

       A1: (A _/\_ B) c= ( Inter (((A ``1 ) /\ (B ``1 )),((A ``2 ) /\ (B ``2 ))))

      proof

        let x be object;

        reconsider xx = x as set by TARSKI: 1;

        assume x in (A _/\_ B);

        then

        consider X,Y be set such that

         A2: X in A & Y in B & x = (X /\ Y) by SETFAM_1:def 5;

        (A ``1 ) c= X & (B ``1 ) c= Y & X c= (A ``2 ) & Y c= (B ``2 ) by A2, Th14;

        then ((A ``1 ) /\ (B ``1 )) c= xx & xx c= ((A ``2 ) /\ (B ``2 )) by A2, XBOOLE_1: 27;

        hence thesis by Th1;

      end;

      ( Inter (((A ``1 ) /\ (B ``1 )),((A ``2 ) /\ (B ``2 )))) c= (A _/\_ B)

      proof

        let x be object;

        assume x in ( Inter (((A ``1 ) /\ (B ``1 )),((A ``2 ) /\ (B ``2 ))));

        then

        consider Z be Element of ( bool U) such that

         A3: x = Z & ((A ``1 ) /\ (B ``1 )) c= Z & Z c= ((A ``2 ) /\ (B ``2 ));

        (A ``1 ) c= ((Z \/ (A ``1 )) /\ (A ``2 ))

        proof

          let x be object;

          assume

           A4: x in (A ``1 );

          assume

           A5: not x in ((Z \/ (A ``1 )) /\ (A ``2 ));

          per cases by A5, XBOOLE_0:def 4;

            suppose not x in (Z \/ (A ``1 ));

            hence thesis by A4, XBOOLE_0:def 3;

          end;

            suppose

             A6: not x in (A ``2 );

            (A ``1 ) c= (A ``2 ) & x in (A ``1 ) by A4, Th16;

            hence thesis by A6;

          end;

        end;

        then (A ``1 ) c= ((Z \/ (A ``1 )) /\ (A ``2 )) & ((Z \/ (A ``1 )) /\ (A ``2 )) c= (A ``2 ) by XBOOLE_1: 17;

        then

         A7: ((Z \/ (A ``1 )) /\ (A ``2 )) in A by Th14;

        (B ``1 ) c= ((Z \/ (B ``1 )) /\ (B ``2 ))

        proof

          let x be object;

          assume

           A8: x in (B ``1 );

          then

           A9: x in (Z \/ (B ``1 )) by XBOOLE_0:def 3;

          (B ``1 ) c= (B ``2 ) by Th16;

          hence thesis by A8, A9, XBOOLE_0:def 4;

        end;

        then (B ``1 ) c= ((Z \/ (B ``1 )) /\ (B ``2 )) & ((Z \/ (B ``1 )) /\ (B ``2 )) c= (B ``2 ) by XBOOLE_1: 17;

        then

         A10: ((Z \/ (B ``1 )) /\ (B ``2 )) in B by Th14;

        (((Z \/ (A ``1 )) /\ (A ``2 )) /\ ((Z \/ (B ``1 )) /\ (B ``2 ))) = ((((A ``2 ) /\ (Z \/ (A ``1 ))) /\ (Z \/ (B ``1 ))) /\ (B ``2 )) by XBOOLE_1: 16

        .= (((A ``2 ) /\ ((Z \/ (A ``1 )) /\ (Z \/ (B ``1 )))) /\ (B ``2 )) by XBOOLE_1: 16

        .= (((A ``2 ) /\ (Z \/ ((A ``1 ) /\ (B ``1 )))) /\ (B ``2 )) by XBOOLE_1: 24

        .= (((A ``2 ) /\ Z) /\ (B ``2 )) by A3, XBOOLE_1: 12

        .= (Z /\ ((A ``2 ) /\ (B ``2 ))) by XBOOLE_1: 16

        .= Z by A3, XBOOLE_1: 28;

        hence thesis by A3, A7, A10, SETFAM_1:def 5;

      end;

      hence thesis by A1;

    end;

    definition

      let U;

      let A, B;

      :: original: =

      redefine

      :: INTERVA1:def7

      pred A = B means (A ``1 ) = (B ``1 ) & (A ``2 ) = (B ``2 );

      compatibility

      proof

        thus A = B implies (A ``1 ) = (B ``1 ) & (A ``2 ) = (B ``2 );

        assume that

         A1: (A ``1 ) = (B ``1 ) and

         A2: (A ``2 ) = (B ``2 );

        

         A3: A c= B

        proof

          let x be object;

          assume

           A4: x in A;

          consider A1,B1 be Subset of U such that

           A5: A = ( Inter (A1,B1)) by Def2;

          consider C1 be Subset of U such that

           A6: A = ( Inter ((A ``1 ),C1)) by Def5;

          

           A7: A1 = (B ``1 ) by A1, A5, Th6, A6;

          consider C2 be Subset of U such that

           A8: B = ( Inter ((B ``1 ),C2)) by Def5;

          consider D1 be Subset of U such that

           A9: A = ( Inter (D1,(A ``2 ))) by Def6;

          

           A10: (B ``2 ) = B1 by A2, A9, A5, Th6;

          consider D2 be Subset of U such that

           A11: B = ( Inter (D2,(B ``2 ))) by Def6;

          thus thesis by A4, A5, A7, A8, A10, A11, Th6;

        end;

        B c= A

        proof

          let x be object;

          assume

           A12: x in B;

          consider A1,B1 be Subset of U such that

           A13: B = ( Inter (A1,B1)) by Def2;

          consider C1 be Subset of U such that

           A14: B = ( Inter ((B ``1 ),C1)) by Def5;

          

           A15: (A ``1 ) = A1 by A1, A14, Th6, A13;

          consider C2 be Subset of U such that

           A16: A = ( Inter ((A ``1 ),C2)) by Def5;

          consider D1 be Subset of U such that

           A17: B = ( Inter (D1,(B ``2 ))) by Def6;

          

           A18: (A ``2 ) = B1 by A2, A17, A13, Th6;

          consider D2 be Subset of U such that

           A19: A = ( Inter (D2,(A ``2 ))) by Def6;

          thus thesis by A12, A13, A15, A16, A18, A19, Th6;

        end;

        hence thesis by A3;

      end;

    end

    theorem :: INTERVA1:19

    (A _\/_ A) = A

    proof

      

       A1: (A _\/_ A) c= A

      proof

        let x be object;

        assume x in (A _\/_ A);

        then

        consider X,Y be set such that

         A2: X in A & Y in A & x = (X \/ Y) by SETFAM_1:def 4;

        

         A3: (A ``1 ) c= X & X c= (A ``2 ) by A2, Th14;

        (A ``1 ) c= Y & Y c= (A ``2 ) by A2, Th14;

        then

         A4: (X \/ Y) c= (A ``2 ) by A3, XBOOLE_1: 8;

        X c= (X \/ Y) by XBOOLE_1: 7;

        then (A ``1 ) c= (X \/ Y) by A3;

        hence thesis by Th14, A4, A2;

      end;

      A c= (A _\/_ A)

      proof

        let x be object;

        reconsider xx = x as set by TARSKI: 1;

        assume

         A5: x in A;

        x = (xx \/ xx);

        hence thesis by A5, SETFAM_1:def 4;

      end;

      hence thesis by A1;

    end;

    theorem :: INTERVA1:20

    (A _/\_ A) = A

    proof

      

       A1: (A _/\_ A) c= A

      proof

        let x be object;

        assume x in (A _/\_ A);

        then

        consider X,Y be set such that

         A2: X in A & Y in A & x = (X /\ Y) by SETFAM_1:def 5;

        

         A3: (A ``1 ) c= X & X c= (A ``2 ) by A2, Th14;

        (A ``1 ) c= Y & Y c= (A ``2 ) by A2, Th14;

        then

         A4: (A ``1 ) c= (X /\ Y) by A3, XBOOLE_1: 19;

        (X /\ Y) c= X by XBOOLE_1: 17;

        then (X /\ Y) c= (A ``2 ) by A3;

        hence thesis by A4, A2, Th14;

      end;

      A c= (A _/\_ A)

      proof

        let x be object;

        reconsider xx = x as set by TARSKI: 1;

        assume

         A5: x in A;

        x = (xx /\ xx);

        hence thesis by A5, SETFAM_1:def 5;

      end;

      hence thesis by A1;

    end;

    theorem :: INTERVA1:21

    (A _\/_ B) = (B _\/_ A);

    theorem :: INTERVA1:22

    (A _/\_ B) = (B _/\_ A);

    theorem :: INTERVA1:23

    

     Th23: ((A _\/_ B) _\/_ C) = (A _\/_ (B _\/_ C))

    proof

      

       A1: ((A _\/_ B) _\/_ C) c= (A _\/_ (B _\/_ C))

      proof

        let x be object;

        assume x in ((A _\/_ B) _\/_ C);

        then

        consider X,Y be set such that

         A2: X in ( UNION (A,B)) & Y in C & x = (X \/ Y) by SETFAM_1:def 4;

        consider Z,W be set such that

         A3: Z in A & W in B & X = (Z \/ W) by A2, SETFAM_1:def 4;

        (W \/ Y) in ( UNION (B,C)) by A2, A3, SETFAM_1:def 4;

        then (Z \/ (W \/ Y)) in ( UNION (A,( UNION (B,C)))) by A3, SETFAM_1:def 4;

        hence thesis by A2, A3, XBOOLE_1: 4;

      end;

      (A _\/_ (B _\/_ C)) c= ((A _\/_ B) _\/_ C)

      proof

        let x be object;

        assume x in (A _\/_ (B _\/_ C));

        then

        consider X,Y be set such that

         A4: X in A & Y in ( UNION (B,C)) & x = (X \/ Y) by SETFAM_1:def 4;

        consider Z,W be set such that

         A5: Z in B & W in C & Y = (Z \/ W) by A4, SETFAM_1:def 4;

        (X \/ Z) in ( UNION (A,B)) by A4, A5, SETFAM_1:def 4;

        then ((X \/ Z) \/ W) in ( UNION (( UNION (A,B)),C)) by A5, SETFAM_1:def 4;

        hence thesis by A4, A5, XBOOLE_1: 4;

      end;

      hence thesis by A1;

    end;

    theorem :: INTERVA1:24

    

     Th24: ((A _/\_ B) _/\_ C) = (A _/\_ (B _/\_ C))

    proof

      

       A1: ((A _/\_ B) _/\_ C) c= (A _/\_ (B _/\_ C))

      proof

        let x be object;

        assume x in ((A _/\_ B) _/\_ C);

        then

        consider X,Y be set such that

         A2: X in ( INTERSECTION (A,B)) & Y in C & x = (X /\ Y) by SETFAM_1:def 5;

        consider Z,W be set such that

         A3: Z in A & W in B & X = (Z /\ W) by A2, SETFAM_1:def 5;

        (W /\ Y) in ( INTERSECTION (B,C)) by A2, A3, SETFAM_1:def 5;

        then (Z /\ (W /\ Y)) in ( INTERSECTION (A,( INTERSECTION (B,C)))) by A3, SETFAM_1:def 5;

        hence thesis by A2, A3, XBOOLE_1: 16;

      end;

      (A _/\_ (B _/\_ C)) c= ((A _/\_ B) _/\_ C)

      proof

        let x be object;

        assume x in (A _/\_ (B _/\_ C));

        then

        consider X,Y be set such that

         A4: X in A & Y in ( INTERSECTION (B,C)) & x = (X /\ Y) by SETFAM_1:def 5;

        consider Z,W be set such that

         A5: Z in B & W in C & Y = (Z /\ W) by A4, SETFAM_1:def 5;

        (X /\ Z) in ( INTERSECTION (A,B)) by A4, A5, SETFAM_1:def 5;

        then ((X /\ Z) /\ W) in ( INTERSECTION (( INTERSECTION (A,B)),C)) by A5, SETFAM_1:def 5;

        hence thesis by A4, A5, XBOOLE_1: 16;

      end;

      hence thesis by A1;

    end;

    

     Lm1: for X be set, A,B,C be Subset-Family of X holds ( UNION (A,( INTERSECTION (B,C)))) c= ( INTERSECTION (( UNION (A,B)),( UNION (A,C))))

    proof

      let X be set, A,B,C be Subset-Family of X;

      let x be object;

      assume x in ( UNION (A,( INTERSECTION (B,C))));

      then

      consider X,Y be set such that

       A1: X in A & Y in ( INTERSECTION (B,C)) & x = (X \/ Y) by SETFAM_1:def 4;

      consider W,Z be set such that

       A2: W in B & Z in C & Y = (W /\ Z) by A1, SETFAM_1:def 5;

      

       A3: x = ((X \/ W) /\ (X \/ Z)) by A1, A2, XBOOLE_1: 24;

      

       A4: (X \/ W) in ( UNION (A,B)) by A1, A2, SETFAM_1:def 4;

      (X \/ Z) in ( UNION (A,C)) by A1, A2, SETFAM_1:def 4;

      hence thesis by A3, A4, SETFAM_1:def 5;

    end;

    definition

      let X be set;

      let F be Subset-Family of X;

      :: INTERVA1:def8

      attr F is ordered means

      : Def8: ex A,B be set st A in F & B in F & for Y be set holds Y in F iff A c= Y & Y c= B;

    end

    registration

      let X be set;

      cluster non empty ordered for Subset-Family of X;

      existence

      proof

        reconsider F = {X} as Subset-Family of X by ZFMISC_1: 68;

        take F;

        ex A,B be set st A in F & B in F & for Y be set holds Y in F iff A c= Y & Y c= B

        proof

          take X, X;

          thus X in F & X in F by TARSKI:def 1;

          let Y be set;

          thus Y in F implies X c= Y & Y c= X by TARSKI:def 1;

          assume X c= Y & Y c= X;

          then X = Y;

          hence thesis by TARSKI:def 1;

        end;

        hence thesis;

      end;

    end

    theorem :: INTERVA1:25

    

     Th25: for A,B be Subset of U st A c= B holds ( Inter (A,B)) is non empty ordered Subset-Family of U

    proof

      let A,B be Subset of U;

      assume

       A1: A c= B;

      consider C,D be set such that

       A2: C = A & D = B;

      C in ( Inter (A,B)) & D in ( Inter (A,B)) & for Y be set holds Y in ( Inter (A,B)) iff C c= Y & Y c= D by A2, Th1, A1;

      hence thesis by Def8;

    end;

    theorem :: INTERVA1:26

    

     Th26: for A be non empty IntervalSet of U holds A is non empty ordered Subset-Family of U

    proof

      let A be non empty IntervalSet of U;

      A = ( Inter ((A ``1 ),(A ``2 ))) & (A ``1 ) c= (A ``2 ) by Th15, Th16;

      hence thesis by Th25;

    end;

    notation

      let X be set;

      synonym min X for meet X;

      synonym max X for union X;

    end

    definition

      let X be set;

      let F be non empty ordered Subset-Family of X;

      :: original: min

      redefine

      func min F -> Element of F ;

      correctness

      proof

        consider A,B be set such that

         A1: A in F & B in F & for Y be set holds Y in F iff A c= Y & Y c= B by Def8;

        for Z1 be set st Z1 in F holds A c= Z1 by A1;

        then

         A2: A c= ( meet F) by SETFAM_1: 5;

        ( meet F) c= B by A1, SETFAM_1: 3;

        hence thesis by A1, A2;

      end;

      :: original: max

      redefine

      func max F -> Element of F ;

      correctness

      proof

        consider A,B be set such that

         A3: A in F & B in F & for Y be set holds Y in F iff A c= Y & Y c= B by Def8;

        

         A4: for Z1 be set st Z1 in F holds Z1 c= B by A3;

        

         A5: A c= ( union F) by A3, ZFMISC_1: 74;

        ( union F) c= B by A4, ZFMISC_1: 76;

        hence thesis by A3, A5;

      end;

    end

    

     Lm2: for X be set, F be non empty ordered Subset-Family of X, G be set st G in F holds G = ( min F) iff for Y be set st Y in F holds G c= Y by SETFAM_1: 3;

    

     Lm3: for X be set, F be non empty ordered Subset-Family of X, G be set st G in F holds G = ( max F) iff for Y be set st Y in F holds Y c= G by ZFMISC_1: 74;

    theorem :: INTERVA1:27

    

     Th27: for A,B be Subset of U, F be ordered non empty Subset-Family of U st F = ( Inter (A,B)) holds ( min F) = A & ( max F) = B

    proof

      let A,B be Subset of U;

      let F be ordered non empty Subset-Family of U;

      assume

       A1: F = ( Inter (A,B));

      then A is Element of F & for Y be set st Y in F holds A c= Y by Th2, Th1;

      then

       A2: A = ( min F) by Lm2;

      B is Element of F & for Y be set st Y in F holds Y c= B by Th2, A1, Th1;

      hence thesis by A2, Lm3;

    end;

    theorem :: INTERVA1:28

    

     Th28: for X,Y be set, A be non empty ordered Subset-Family of X holds Y in A iff ( min A) c= Y & Y c= ( max A)

    proof

      let X,Y be set;

      let A be non empty ordered Subset-Family of X;

      ( min A) c= Y & Y c= ( max A) implies Y in A

      proof

        assume

         A1: ( min A) c= Y & Y c= ( max A);

        consider C,D be set such that

         A2: C in A & D in A & for X be set holds X in A iff C c= X & X c= D by Def8;

        

         A3: ( min A) c= C & D c= ( max A) by Lm2, Lm3, A2;

        C c= ( min A) & ( max A) c= D by A2;

        then ( min A) = C & ( max A) = D by A3;

        hence thesis by A2, A1;

      end;

      hence thesis by Lm2, Lm3;

    end;

    

     Lm4: for A be non empty IntervalSet of U holds A is non empty ordered Subset-Family of U by Th26;

    theorem :: INTERVA1:29

    

     Th29: for X be set, A,B,C be non empty ordered Subset-Family of X holds ( UNION (A,( INTERSECTION (B,C)))) = ( INTERSECTION (( UNION (A,B)),( UNION (A,C))))

    proof

      let X be set, A,B,C be non empty ordered Subset-Family of X;

      

       A1: ( UNION (A,( INTERSECTION (B,C)))) c= ( INTERSECTION (( UNION (A,B)),( UNION (A,C)))) by Lm1;

      ( INTERSECTION (( UNION (A,B)),( UNION (A,C)))) c= ( UNION (A,( INTERSECTION (B,C))))

      proof

        let x be object;

        assume x in ( INTERSECTION (( UNION (A,B)),( UNION (A,C))));

        then

        consider X,Y be set such that

         A2: X in ( UNION (A,B)) & Y in ( UNION (A,C)) & x = (X /\ Y) by SETFAM_1:def 5;

        consider X1,X2 be set such that

         A3: X1 in A & X2 in B & X = (X1 \/ X2) by A2, SETFAM_1:def 4;

        consider Y1,Y2 be set such that

         A4: Y1 in A & Y2 in C & Y = (Y1 \/ Y2) by A2, SETFAM_1:def 4;

        

         A5: x = ((X1 /\ (Y1 \/ Y2)) \/ (X2 /\ (Y1 \/ Y2))) by A2, A3, A4, XBOOLE_1: 23

        .= (((X1 /\ Y1) \/ (X1 /\ Y2)) \/ (X2 /\ (Y1 \/ Y2))) by XBOOLE_1: 23

        .= (((X1 /\ Y1) \/ (X1 /\ Y2)) \/ ((X2 /\ Y1) \/ (X2 /\ Y2))) by XBOOLE_1: 23

        .= ((((X1 /\ Y1) \/ (X1 /\ Y2)) \/ (X2 /\ Y1)) \/ (X2 /\ Y2)) by XBOOLE_1: 4;

        set A1 = ( min A), A2 = ( max A);

        A1 c= X1 & X1 c= A2 & A1 c= Y1 & Y1 c= A2 by A3, A4, Th28;

        then

         A6: (A1 /\ A1) c= (X1 /\ Y1) & (X1 /\ Y1) c= (A2 /\ A2) by XBOOLE_1: 27;

        Y1 c= A2 & (X2 /\ Y1) c= Y1 by A4, Th28, XBOOLE_1: 17;

        then (X2 /\ Y1) c= A2;

        then

         A7: A1 c= ((X1 /\ Y1) \/ (X2 /\ Y1)) & ((X1 /\ Y1) \/ (X2 /\ Y1)) c= A2 by A6, XBOOLE_1: 8, XBOOLE_1: 10;

        X1 c= A2 & (X1 /\ Y2) c= X1 by A3, Th28, XBOOLE_1: 17;

        then (X1 /\ Y2) c= A2;

        then (((X1 /\ Y1) \/ (X2 /\ Y1)) \/ (X1 /\ Y2)) c= A2 by A7, XBOOLE_1: 8;

        then A1 c= (((X1 /\ Y1) \/ (X2 /\ Y1)) \/ (X1 /\ Y2)) & (((X1 /\ Y1) \/ (X1 /\ Y2)) \/ (X2 /\ Y1)) c= A2 by A7, XBOOLE_1: 4, XBOOLE_1: 10;

        then A1 c= (((X1 /\ Y1) \/ (X1 /\ Y2)) \/ (X2 /\ Y1)) & (((X1 /\ Y1) \/ (X1 /\ Y2)) \/ (X2 /\ Y1)) c= A2 by XBOOLE_1: 4;

        then

         A8: (((X1 /\ Y1) \/ (X1 /\ Y2)) \/ (X2 /\ Y1)) in A by Th28;

        (X2 /\ Y2) in ( INTERSECTION (B,C)) by A3, A4, SETFAM_1:def 5;

        hence thesis by A8, A5, SETFAM_1:def 4;

      end;

      hence thesis by A1;

    end;

    

     Lm5: for X be set, A,B,C be Subset-Family of X holds ( INTERSECTION (A,( UNION (B,C)))) c= ( UNION (( INTERSECTION (A,B)),( INTERSECTION (A,C))))

    proof

      let X be set, A,B,C be Subset-Family of X;

      let x be object;

      assume x in ( INTERSECTION (A,( UNION (B,C))));

      then

      consider X,Y be set such that

       A1: X in A & Y in ( UNION (B,C)) & x = (X /\ Y) by SETFAM_1:def 5;

      consider Z,W be set such that

       A2: Z in B & W in C & Y = (Z \/ W) by A1, SETFAM_1:def 4;

      

       A3: x = ((X /\ Z) \/ (X /\ W)) by A1, A2, XBOOLE_1: 23;

      

       A4: (X /\ Z) in ( INTERSECTION (A,B)) by A1, A2, SETFAM_1:def 5;

      (X /\ W) in ( INTERSECTION (A,C)) by A1, A2, SETFAM_1:def 5;

      hence thesis by A3, A4, SETFAM_1:def 4;

    end;

    theorem :: INTERVA1:30

    

     Th30: for X be set, A,B,C be non empty ordered Subset-Family of X holds ( INTERSECTION (A,( UNION (B,C)))) = ( UNION (( INTERSECTION (A,B)),( INTERSECTION (A,C))))

    proof

      let X be set, A,B,C be non empty ordered Subset-Family of X;

      

       A1: ( INTERSECTION (A,( UNION (B,C)))) c= ( UNION (( INTERSECTION (A,B)),( INTERSECTION (A,C)))) by Lm5;

      ( UNION (( INTERSECTION (A,B)),( INTERSECTION (A,C)))) c= ( INTERSECTION (A,( UNION (B,C))))

      proof

        let x be object;

        assume x in ( UNION (( INTERSECTION (A,B)),( INTERSECTION (A,C))));

        then

        consider X,Y be set such that

         A2: X in ( INTERSECTION (A,B)) & Y in ( INTERSECTION (A,C)) & x = (X \/ Y) by SETFAM_1:def 4;

        consider X1,X2 be set such that

         A3: X1 in A & X2 in B & X = (X1 /\ X2) by A2, SETFAM_1:def 5;

        consider Y1,Y2 be set such that

         A4: Y1 in A & Y2 in C & Y = (Y1 /\ Y2) by A2, SETFAM_1:def 5;

        

         A5: x = (((X1 /\ X2) \/ Y1) /\ ((X1 /\ X2) \/ Y2)) by A2, A3, A4, XBOOLE_1: 24

        .= ((Y1 \/ (X1 /\ X2)) /\ ((Y2 \/ X1) /\ (Y2 \/ X2))) by XBOOLE_1: 24

        .= (((Y1 \/ X1) /\ (Y1 \/ X2)) /\ ((Y2 \/ X1) /\ (Y2 \/ X2))) by XBOOLE_1: 24

        .= ((((Y1 \/ X1) /\ (Y1 \/ X2)) /\ (Y2 \/ X1)) /\ (Y2 \/ X2)) by XBOOLE_1: 16;

        set A1 = ( min A), A2 = ( max A);

        

         A6: A1 c= Y1 & A1 c= X1 by A3, A4, Th28;

        then

         A7: (A1 \/ A1) c= (Y1 \/ X1) by XBOOLE_1: 13;

        Y1 c= (Y1 \/ X2) by XBOOLE_1: 7;

        then A1 c= (Y1 \/ X2) by A6;

        then

         A8: (A1 /\ A1) c= ((Y1 \/ X1) /\ (Y1 \/ X2)) by A7, XBOOLE_1: 27;

        A1 c= X1 & X1 c= (Y2 \/ X1) by Th28, A3, XBOOLE_1: 7;

        then A1 c= (Y2 \/ X1);

        then

         A9: A1 c= (((Y1 \/ X1) /\ (Y1 \/ X2)) /\ (Y2 \/ X1)) by A8, XBOOLE_1: 19;

        Y1 c= A2 & X1 c= A2 by A3, A4, Th28;

        then ((Y1 \/ X1) /\ ((Y1 \/ X2) /\ (Y2 \/ X1))) c= (Y1 \/ X1) & (Y1 \/ X1) c= A2 by XBOOLE_1: 8, XBOOLE_1: 17;

        then A1 c= (((Y1 \/ X1) /\ (Y1 \/ X2)) /\ (Y2 \/ X1)) & ((Y1 \/ X1) /\ ((Y1 \/ X2) /\ (Y2 \/ X1))) c= A2 by A9;

        then A1 c= (((Y1 \/ X1) /\ (Y1 \/ X2)) /\ (Y2 \/ X1)) & (((Y1 \/ X1) /\ (Y1 \/ X2)) /\ (Y2 \/ X1)) c= A2 by XBOOLE_1: 16;

        then

         A10: (((Y1 \/ X1) /\ (Y1 \/ X2)) /\ (Y2 \/ X1)) in A by Th28;

        (Y2 \/ X2) in ( UNION (B,C)) by A3, A4, SETFAM_1:def 4;

        hence thesis by A5, A10, SETFAM_1:def 5;

      end;

      hence thesis by A1;

    end;

    theorem :: INTERVA1:31

    (A _\/_ (B _/\_ C)) = ((A _\/_ B) _/\_ (A _\/_ C))

    proof

      

       A1: (A _\/_ (B _/\_ C)) c= ((A _\/_ B) _/\_ (A _\/_ C)) by Lm1;

      ((A _\/_ B) _/\_ (A _\/_ C)) c= (A _\/_ (B _/\_ C))

      proof

        let x be object;

        assume x in ((A _\/_ B) _/\_ (A _\/_ C));

        then

        consider X,Y be set such that

         A2: X in ( UNION (A,B)) & Y in ( UNION (A,C)) & x = (X /\ Y) by SETFAM_1:def 5;

        

         A3: A is non empty ordered Subset-Family of U & B is non empty ordered Subset-Family of U & C is non empty ordered Subset-Family of U by Lm4;

        x in ( INTERSECTION (( UNION (A,B)),( UNION (A,C)))) by A2, SETFAM_1:def 5;

        hence thesis by Th29, A3;

      end;

      hence thesis by A1;

    end;

    theorem :: INTERVA1:32

    (A _/\_ (B _\/_ C)) = ((A _/\_ B) _\/_ (A _/\_ C))

    proof

      

       A1: (A _/\_ (B _\/_ C)) c= ((A _/\_ B) _\/_ (A _/\_ C))

      proof

        let x be object;

        assume x in (A _/\_ (B _\/_ C));

        then

        consider X,Y be set such that

         A2: X in A & Y in ( UNION (B,C)) & x = (X /\ Y) by SETFAM_1:def 5;

        consider Z,W be set such that

         A3: Z in B & W in C & Y = (Z \/ W) by A2, SETFAM_1:def 4;

        

         A4: A is non empty ordered Subset-Family of U & B is non empty ordered Subset-Family of U & C is non empty ordered Subset-Family of U by Lm4;

        (X /\ (Z \/ W)) in ( INTERSECTION (A,( UNION (B,C)))) by A2, A3, SETFAM_1:def 5;

        hence thesis by A2, A3, Th30, A4;

      end;

      ((A _/\_ B) _\/_ (A _/\_ C)) c= (A _/\_ (B _\/_ C))

      proof

        let x be object;

        assume x in ((A _/\_ B) _\/_ (A _/\_ C));

        then

        consider X,Y be set such that

         A5: X in ( INTERSECTION (A,B)) & Y in ( INTERSECTION (A,C)) & x = (X \/ Y) by SETFAM_1:def 4;

        

         A6: A is non empty ordered Subset-Family of U & B is non empty ordered Subset-Family of U & C is non empty ordered Subset-Family of U by Lm4;

        x in ( UNION (( INTERSECTION (A,B)),( INTERSECTION (A,C)))) by A5, SETFAM_1:def 4;

        hence thesis by Th30, A6;

      end;

      hence thesis by A1;

    end;

    theorem :: INTERVA1:33

    

     Th33: for X be set, A,B be non empty ordered Subset-Family of X holds ( INTERSECTION (A,( UNION (A,B)))) = A

    proof

      let X be set;

      let A,B be non empty ordered Subset-Family of X;

      set A1 = ( min A), A2 = ( max A);

      

       A1: ( INTERSECTION (A,( UNION (A,B)))) c= A

      proof

        let x be object;

        assume x in ( INTERSECTION (A,( UNION (A,B))));

        then

        consider Y,Z be set such that

         A2: Y in A & Z in ( UNION (A,B)) & x = (Y /\ Z) by SETFAM_1:def 5;

        consider Z1,Z2 be set such that

         A3: Z1 in A & Z2 in B & Z = (Z1 \/ Z2) by A2, SETFAM_1:def 4;

        

         A4: x = ((Y /\ Z1) \/ (Y /\ Z2)) by A2, A3, XBOOLE_1: 23;

        

         A5: (A1 c= Y & Y c= A2) & (A1 c= Z1 & Z1 c= A2) by Th28, A2, A3;

        then A1 c= (Y /\ Z1) & (Y /\ Z1) c= (A2 /\ A2) by XBOOLE_1: 19, XBOOLE_1: 27;

        then

         A6: A1 c= (Y /\ Z1) & (Y /\ Z1) c= A2 & (Y /\ Z1) c= ((Y /\ Z1) \/ (Y /\ Z2)) by XBOOLE_1: 7;

        then

         A7: A1 c= ((Y /\ Z1) \/ (Y /\ Z2));

        (Y /\ Z2) c= Y by XBOOLE_1: 17;

        then (Y /\ Z2) c= A2 by A5;

        then ((Y /\ Z1) \/ (Y /\ Z2)) c= A2 by A6, XBOOLE_1: 8;

        hence thesis by Th28, A4, A7;

      end;

      A c= ( INTERSECTION (A,( UNION (A,B))))

      proof

        let x be object;

        reconsider xx = x as set by TARSKI: 1;

        assume

         A8: x in A;

        set b = the Element of B;

        

         A9: x = (xx /\ (xx \/ b)) by XBOOLE_1: 21;

        (xx \/ b) in ( UNION (A,B)) by A8, SETFAM_1:def 4;

        hence thesis by A8, A9, SETFAM_1:def 5;

      end;

      hence thesis by A1;

    end;

    theorem :: INTERVA1:34

    

     Th34: for X be set, A,B be non empty ordered Subset-Family of X holds ( UNION (( INTERSECTION (A,B)),B)) = B

    proof

      let X be set;

      let A,B be non empty ordered Subset-Family of X;

      

       A1: ( UNION (( INTERSECTION (A,B)),B)) c= B

      proof

        let x be object;

        reconsider xx = x as set by TARSKI: 1;

        set B1 = ( min B), B2 = ( max B);

        assume x in ( UNION (( INTERSECTION (A,B)),B));

        then

        consider Y,Z be set such that

         A2: Y in ( INTERSECTION (A,B)) & Z in B & x = (Y \/ Z) by SETFAM_1:def 4;

        consider Y1,Y2 be set such that

         A3: Y1 in A & Y2 in B & Y = (Y1 /\ Y2) by A2, SETFAM_1:def 5;

        B1 c= Y2 & Y2 c= B2 & (Y1 /\ Y2) c= Y2 by A3, Th28, XBOOLE_1: 17;

        then

         A4: (Y1 /\ Y2) c= B2;

        Z c= B2 by A2, Th28;

        then

         A5: xx c= B2 by A2, A3, A4, XBOOLE_1: 8;

        B1 c= Z & Z c= xx by A2, Th28, XBOOLE_1: 7;

        then B1 c= xx & xx c= B2 by A5;

        hence thesis by Th28;

      end;

      B c= ( UNION (( INTERSECTION (A,B)),B))

      proof

        let x be object;

        reconsider xx = x as set by TARSKI: 1;

        assume

         A6: x in B;

        set b = the Element of A;

        

         A7: x = (xx \/ (xx /\ b)) by XBOOLE_1: 22;

        (b /\ xx) in ( INTERSECTION (A,B)) by A6, SETFAM_1:def 5;

        hence thesis by A7, A6, SETFAM_1:def 4;

      end;

      hence thesis by A1;

    end;

    theorem :: INTERVA1:35

    

     Th35: (A _/\_ (A _\/_ B)) = A

    proof

      A is non empty ordered Subset-Family of U & B is non empty ordered Subset-Family of U by Lm4;

      hence thesis by Th33;

    end;

    theorem :: INTERVA1:36

    

     Th36: ((A _/\_ B) _\/_ B) = B

    proof

      A is non empty ordered Subset-Family of U & B is non empty ordered Subset-Family of U by Lm4;

      hence thesis by Th34;

    end;

    begin

    theorem :: INTERVA1:37

    

     Th37: for U be non empty set, A,B be Subset-Family of U holds ( DIFFERENCE (A,B)) is Subset-Family of U

    proof

      let U be non empty set, A,B be Subset-Family of U;

      ( DIFFERENCE (A,B)) c= ( bool U)

      proof

        let x be object;

        assume x in ( DIFFERENCE (A,B));

        then

        consider Y,Z be set such that

         A1: Y in A & Z in B & x = (Y \ Z) by SETFAM_1:def 6;

        (Y \ Z) c= U by A1, XBOOLE_1: 109;

        hence thesis by A1;

      end;

      hence thesis;

    end;

    theorem :: INTERVA1:38

    

     Th38: for U be non empty set, A,B be non empty ordered Subset-Family of U holds ( DIFFERENCE (A,B)) = { C where C be Subset of U : (( min A) \ ( max B)) c= C & C c= (( max A) \ ( min B)) }

    proof

      let U be non empty set;

      let A,B be non empty ordered Subset-Family of U;

      set A1 = ( min A), B1 = ( min B), A2 = ( max A), B2 = ( max B);

      

       A1: ( DIFFERENCE (A,B)) c= { C where C be Subset of U : (( min A) \ ( max B)) c= C & C c= (( max A) \ ( min B)) }

      proof

        let x be object;

        assume

         A2: x in ( DIFFERENCE (A,B));

        then

        consider Y,Z be set such that

         A3: Y in A & Z in B & x = (Y \ Z) by SETFAM_1:def 6;

        ( DIFFERENCE (A,B)) is Subset-Family of U by Th37;

        then

        reconsider x as Subset of U by A2;

        A1 c= Y & Y c= A2 & B1 c= Z & Z c= B2 by A3, Th28;

        then (A1 \ B2) c= x & x c= (A2 \ B1) by A3, XBOOLE_1: 35;

        hence thesis;

      end;

      { C where C be Subset of U : (( min A) \ ( max B)) c= C & C c= (( max A) \ ( min B)) } c= ( DIFFERENCE (A,B))

      proof

        let x be object;

        assume x in { C where C be Subset of U : (( min A) \ ( max B)) c= C & C c= (( max A) \ ( min B)) };

        then

        consider x9 be Subset of U such that

         A4: x9 = x & (( min A) \ ( max B)) c= x9 & x9 c= (( max A) \ ( min B));

        set A1 = ( min A), A2 = ( max A), B1 = ( min B), B2 = ( max B);

        set z1 = ((x9 \/ A1) /\ A2);

        set z2 = (((x9 \/ (B2 ` )) /\ (B1 ` )) ` );

        B1 c= B2 by Lm2;

        then

         A5: (B2 ` ) c= (B1 ` ) by SUBSET_1: 12;

        ((x9 \/ (B2 ` )) /\ (B1 ` )) = ((x9 /\ (B1 ` )) \/ ((B2 ` ) /\ (B1 ` ))) by XBOOLE_1: 23

        .= ((x9 /\ (B1 ` )) \/ (B2 ` )) by A5, XBOOLE_1: 28;

        then

         A6: (B2 ` ) c= ((x9 \/ (B2 ` )) /\ (B1 ` )) by XBOOLE_1: 7;

        ((x9 \/ (B2 ` )) /\ (B1 ` )) c= (B1 ` ) by XBOOLE_1: 17;

        then

         A7: (((x9 \/ (B2 ` )) /\ (B1 ` )) ` ) c= ((B2 ` ) ` ) & ((B1 ` ) ` ) c= (((x9 \/ (B2 ` )) /\ (B1 ` )) ` ) by A6, SUBSET_1: 12;

        z1 = ((x9 /\ A2) \/ (A1 /\ A2)) by XBOOLE_1: 23

        .= ((x9 /\ A2) \/ A1) by SETFAM_1: 2, XBOOLE_1: 28;

        then A1 c= z1 & z1 c= A2 by XBOOLE_1: 7, XBOOLE_1: 17;

        then

         A8: z1 in A & z2 in B by Th28, A7;

        

         A9: ((x9 \/ (A1 \ B2)) /\ (A2 \ B1)) = (x9 /\ (A2 \ B1)) by A4, XBOOLE_1: 12

        .= x9 by A4, XBOOLE_1: 28;

        (z1 \ z2) = (z1 /\ (z2 ` )) by SUBSET_1: 13

        .= ((x9 \/ A1) /\ (A2 /\ ((x9 \/ (B2 ` )) /\ (B1 ` )))) by XBOOLE_1: 16

        .= ((x9 \/ A1) /\ ((x9 \/ (B2 ` )) /\ ((B1 ` ) /\ A2))) by XBOOLE_1: 16

        .= ((x9 \/ A1) /\ ((x9 \/ (B2 ` )) /\ (A2 \ B1))) by SUBSET_1: 13

        .= (((x9 \/ A1) /\ (x9 \/ (B2 ` ))) /\ (A2 \ B1)) by XBOOLE_1: 16

        .= ((x9 \/ (A1 /\ (B2 ` ))) /\ (A2 \ B1)) by XBOOLE_1: 24

        .= x9 by A9, SUBSET_1: 13;

        hence thesis by A4, A8, SETFAM_1:def 6;

      end;

      hence thesis by A1;

    end;

    theorem :: INTERVA1:39

    

     Th39: for U be non empty set, A1,A2,B1,B2 be Subset of U st A1 c= A2 & B1 c= B2 holds ( DIFFERENCE (( Inter (A1,A2)),( Inter (B1,B2)))) = { C where C be Subset of U : (A1 \ B2) c= C & C c= (A2 \ B1) }

    proof

      let U be non empty set;

      let A1,A2,B1,B2 be Subset of U;

      assume A1 c= A2 & B1 c= B2;

      then

      reconsider A12 = ( Inter (A1,A2)), B12 = ( Inter (B1,B2)) as non empty ordered Subset-Family of U by Th25;

      

       A1: ( min A12) = A1 & ( max A12) = A2 by Th27;

      ( min B12) = B1 & ( max B12) = B2 by Th27;

      hence thesis by Th38, A1;

    end;

    definition

      let U be non empty set, A,B be non empty IntervalSet of U;

      :: INTERVA1:def9

      func A _\_ B -> IntervalSet of U equals ( DIFFERENCE (A,B));

      coherence

      proof

        set IT = ( DIFFERENCE (A,B));

        consider A1,A2 be Subset of U such that

         A1: A1 c= A2 & A = ( Inter (A1,A2)) by Th11;

        consider B1,B2 be Subset of U such that

         A2: B1 c= B2 & B = ( Inter (B1,B2)) by Th11;

        set LAB = (A1 \ B2);

        set UAB = (A2 \ B1);

        IT = ( Inter (LAB,UAB)) by Th39, A1, A2;

        hence thesis;

      end;

    end

    registration

      let U be non empty set, A,B be non empty IntervalSet of U;

      cluster (A _\_ B) -> non empty;

      coherence

      proof

        (A _\_ B) <> {}

        proof

          assume

           A1: (A _\_ B) = {} ;

          consider A1,A2 be Subset of U such that

           A2: A1 c= A2 & A = ( Inter (A1,A2)) by Th11;

          consider B1,B2 be Subset of U such that

           A3: B1 c= B2 & B = ( Inter (B1,B2)) by Th11;

          consider y be set such that

           A4: y = (A1 \ B1);

           not (A1 in A & B1 in B & y = (A1 \ B1)) by A1, SETFAM_1:def 6;

          hence thesis by A4, A2, A3;

        end;

        hence thesis;

      end;

    end

    theorem :: INTERVA1:40

    

     Th40: (A _\_ B) = ( Inter (((A ``1 ) \ (B ``2 )),((A ``2 ) \ (B ``1 ))))

    proof

      reconsider AA = A, BB = B as non empty ordered Subset-Family of U by Th26;

      AA = ( Inter ((A ``1 ),(A ``2 ))) & BB = ( Inter ((B ``1 ),(B ``2 ))) by Th15;

      then ( min AA) = (A ``1 ) & ( min BB) = (B ``1 ) & ( max AA) = (A ``2 ) & ( max BB) = (B ``2 ) by Th27;

      hence thesis by Th38;

    end;

    theorem :: INTERVA1:41

    

     Th41: for X,Y be Subset of U st A = ( Inter (X,Y)) holds (A _\_ C) = ( Inter ((X \ (C ``2 )),(Y \ (C ``1 ))))

    proof

      let X,Y be Subset of U;

      assume

       A1: A = ( Inter (X,Y));

      A = ( Inter ((A ``1 ),(A ``2 ))) by Th15;

      then X = (A ``1 ) & Y = (A ``2 ) by A1, Th6;

      hence thesis by Th40;

    end;

    theorem :: INTERVA1:42

    

     Th42: for X,Y,W,Z be Subset of U st A = ( Inter (X,Y)) & C = ( Inter (W,Z)) holds (A _\_ C) = ( Inter ((X \ Z),(Y \ W)))

    proof

      let X,Y,W,Z be Subset of U;

      assume

       A1: A = ( Inter (X,Y)) & C = ( Inter (W,Z));

      A = ( Inter ((A ``1 ),(A ``2 ))) & C = ( Inter ((C ``1 ),(C ``2 ))) by Th15;

      then (A ``1 ) = X & (A ``2 ) = Y & (C ``1 ) = W & (C ``2 ) = Z by A1, Th6;

      hence thesis by Th40;

    end;

    theorem :: INTERVA1:43

    

     Th43: for U be non empty set holds ( Inter (( [#] U),( [#] U))) is non empty IntervalSet of U

    proof

      let U be non empty set;

      ( Inter (( [#] U),( [#] U))) = {( [#] U)} by Th8;

      hence thesis;

    end;

    theorem :: INTERVA1:44

    

     Th44: for U be non empty set holds ( Inter (( {} U),( {} U))) is non empty IntervalSet of U

    proof

      let U be non empty set;

      ( Inter (( {} U),( {} U))) = { {} } by Th8;

      hence thesis;

    end;

    registration

      let U be non empty set;

      cluster ( Inter (( [#] U),( [#] U))) -> non empty;

      coherence by Th43;

      cluster ( Inter (( {} U),( {} U))) -> non empty;

      coherence by Th44;

    end

    definition

      let U be non empty set, A be non empty IntervalSet of U;

      :: INTERVA1:def10

      func A ^ -> non empty IntervalSet of U equals (( Inter (( [#] U),( [#] U))) _\_ A);

      coherence ;

    end

    theorem :: INTERVA1:45

    

     Th45: for U be non empty set, A be non empty IntervalSet of U holds (A ^ ) = ( Inter (((A ``2 ) ` ),((A ``1 ) ` ))) by Th41;

    theorem :: INTERVA1:46

    

     Th46: for X,Y be Subset of U st A = ( Inter (X,Y)) & X c= Y holds (A ^ ) = ( Inter ((Y ` ),(X ` )))

    proof

      let X,Y be Subset of U;

      assume

       A1: A = ( Inter (X,Y)) & X c= Y;

      then ( Inter (X,Y)) = ( Inter ((A ``1 ),(A ``2 ))) by Th15;

      then X = (A ``1 ) & Y = (A ``2 ) by Th6, A1;

      hence thesis by Th41;

    end;

    theorem :: INTERVA1:47

    (( Inter (( {} U),( {} U))) ^ ) = ( Inter (( [#] U),( [#] U)))

    proof

      (( Inter (( {} U),( {} U))) ^ ) = ( Inter (( [#] U),(( {} U) ` ))) by Th46;

      hence thesis;

    end;

    theorem :: INTERVA1:48

    (( Inter (( [#] U),( [#] U))) ^ ) = ( Inter (( {} U),( {} U)))

    proof

      (( Inter (( [#] U),( [#] U))) ^ ) = ( Inter ((( [#] U) ` ),(( [#] U) ` ))) by Th46

      .= ( Inter (( {} U),(( [#] U) ` ))) by XBOOLE_1: 37;

      hence thesis by XBOOLE_1: 37;

    end;

    begin

    theorem :: INTERVA1:49

    ex A be non empty IntervalSet of U st ((A _/\_ A) ^ ) <> ( Inter (( {} U),( {} U)))

    proof

      

       A1: ( [#] U) in ( Inter (( {} U),( [#] U)));

      then

      consider A be non empty IntervalSet of U such that

       A2: A = ( Inter (( {} U),( [#] U)));

      

       A3: (A ^ ) = ( Inter ((( [#] U) ` ),(( {} U) ` ))) by A2, Th46

      .= ( Inter (( {} U),( [#] U)));

      (A ^ ) = ( Inter (((A ^ ) ``1 ),((A ^ ) ``2 ))) by Th15;

      then ((A ^ ) ``1 ) = ( {} U) & ((A ^ ) ``2 ) = ( [#] U) by Th6, A3;

      

      then

       A4: ((A _/\_ A) ^ ) = ( Inter ((( {} U) /\ ( {} U)),(( [#] U) /\ ( [#] U)))) by A2, Th18, A3

      .= ( Inter (( {} U),( [#] U)));

       not ( [#] U) c= ( {} U);

      then not ( [#] U) in ( Inter (( {} U),( {} U))) by Th1;

      hence thesis by A4, A1;

    end;

    theorem :: INTERVA1:50

    ex A be non empty IntervalSet of U st ((A _\/_ A) ^ ) <> ( Inter (( [#] U),( [#] U)))

    proof

       not ( [#] U) c= ( {} U);

      then

       A1: not ( {} U) in ( Inter (( [#] U),( [#] U))) by Th1;

      

       A2: ( {} U) in ( Inter (( {} U),( [#] U)));

      then

      consider A be non empty IntervalSet of U such that

       A3: A = ( Inter (( {} U),( [#] U)));

      

       A4: (A ^ ) = ( Inter ((( [#] U) ` ),(( {} U) ` ))) by Th46, A3

      .= ( Inter (( {} U),( [#] U)));

      (A ^ ) = ( Inter (((A ^ ) ``1 ),((A ^ ) ``2 ))) by Th15;

      then ((A ^ ) ``1 ) = ( {} U) & ((A ^ ) ``2 ) = ( [#] U) by Th6, A4;

      

      then ((A _\/_ A) ^ ) = ( Inter ((( {} U) \/ ( {} U)),(( [#] U) \/ ( [#] U)))) by Th17, A3, A4

      .= ( Inter (( {} U),( [#] U)));

      hence thesis by A2, A1;

    end;

    theorem :: INTERVA1:51

    ex A be non empty IntervalSet of U st (A _\_ A) <> ( Inter (( {} U),( {} U)))

    proof

      ( Inter (( {} U),( [#] U))) <> {} by Th1;

      then

      consider A be non empty IntervalSet of U such that

       A1: A = ( Inter (( {} U),( [#] U)));

      

       A2: (A _\_ A) = ( Inter ((( {} U) \ ( [#] U)),(( [#] U) \ ( {} U)))) by Th42, A1

      .= ( Inter (( {} U),( [#] U)));

       not U c= {} ;

      then ( [#] U) in ( Inter (( {} U),( [#] U))) & not ( [#] U) in ( Inter (( {} U),( {} U))) by Th1;

      hence thesis by A2;

    end;

    theorem :: INTERVA1:52

    for A be non empty IntervalSet of U holds U in (A _\/_ (A ^ ))

    proof

      let A be non empty IntervalSet of U;

      

       A1: U c= ((A ``2 ) \/ ((A ``1 ) ` ))

      proof

        let x be object;

        assume

         A2: x in U;

        (A ``1 ) c= (A ``2 ) by Th16;

        then

         A3: ((A ``2 ) ` ) c= ((A ``1 ) ` ) by SUBSET_1: 12;

        x in (A ``2 ) or x in ((A ``2 ) ` ) by A2, XBOOLE_0:def 5;

        hence thesis by A3, XBOOLE_0:def 3;

      end;

      

       A4: (A ^ ) = ( Inter (((A ``2 ) ` ),((A ``1 ) ` ))) by Th45;

      (A ^ ) = ( Inter (((A ^ ) ``1 ),((A ^ ) ``2 ))) by Th15;

      then ((A ^ ) ``1 ) = ((A ``2 ) ` ) & ((A ^ ) ``2 ) = ((A ``1 ) ` ) by Th6, A4;

      then (A _\/_ (A ^ )) = ( Inter (((A ``1 ) \/ ((A ``2 ) ` )),((A ``2 ) \/ ((A ``1 ) ` )))) by Th17;

      hence thesis by A1;

    end;

    theorem :: INTERVA1:53

    for A be non empty IntervalSet of U holds {} in (A _/\_ (A ^ ))

    proof

      let A be non empty IntervalSet of U;

      

       A1: ((A ``1 ) /\ ((A ``2 ) ` )) c= {}

      proof

        let x be object;

        

         A2: (A ``1 ) c= (A ``2 ) by Th16;

        assume x in ((A ``1 ) /\ ((A ``2 ) ` ));

        then x in (A ``1 ) & x in ((A ``2 ) ` ) by XBOOLE_0:def 4;

        hence thesis by A2, XBOOLE_0:def 5;

      end;

      

       A3: (A ^ ) = ( Inter (((A ``2 ) ` ),((A ``1 ) ` ))) by Th45;

      (A ^ ) = ( Inter (((A ^ ) ``1 ),((A ^ ) ``2 ))) by Th15;

      then ((A ^ ) ``1 ) = ((A ``2 ) ` ) & ((A ^ ) ``2 ) = ((A ``1 ) ` ) by Th6, A3;

      then

       A4: (A _/\_ (A ^ )) = ( Inter (((A ``1 ) /\ ((A ``2 ) ` )),((A ``2 ) /\ ((A ``1 ) ` )))) by Th18;

      ((A ``1 ) /\ ((A ``2 ) ` )) c= {} & {} c= ((A ``2 ) /\ ((A ``1 ) ` )) by A1;

      hence thesis by A4, Th1;

    end;

    theorem :: INTERVA1:54

    for A be non empty IntervalSet of U holds {} in (A _\_ A)

    proof

      let A be non empty IntervalSet of U;

      

       A1: (A _\_ A) = ( Inter (((A ``1 ) \ (A ``2 )),((A ``2 ) \ (A ``1 )))) by Th40;

      

       A2: ((A ``1 ) \ (A ``2 )) c= {}

      proof

        let x be object;

        assume x in ((A ``1 ) \ (A ``2 ));

        then x in (A ``1 ) & not x in (A ``2 ) & (A ``1 ) c= (A ``2 ) by Th16, XBOOLE_0:def 5;

        hence thesis;

      end;

       {} c= ((A ``2 ) \ (A ``1 ));

      hence thesis by Th1, A2, A1;

    end;

    begin

    definition

      let U be non empty set;

      :: INTERVA1:def11

      func IntervalSets U -> non empty set means

      : Def11: for x be set holds x in it iff x is non empty IntervalSet of U;

      existence

      proof

        defpred P[ set] means $1 is non empty IntervalSet of U;

        ex X be set st for x be set holds x in X iff x in ( bool ( bool U)) & P[x] from XFAMILY:sch 1;

        then

        consider X be set such that

         A1: for x be set holds x in X iff x in ( bool ( bool U)) & P[x];

        set x = the Element of U;

        reconsider E = {x} as Subset of U by ZFMISC_1: 31;

         {E} is non empty IntervalSet of U by Th10;

        then

        reconsider X as non empty set by A1;

        take X;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let S1,S2 be non empty set such that

         A2: for x be set holds x in S1 iff x is non empty IntervalSet of U and

         A3: for x be set holds x in S2 iff x is non empty IntervalSet of U;

        for x be object holds x in S1 iff x in S2 by A3, A2;

        hence thesis by TARSKI: 2;

      end;

    end

    definition

      let U be non empty set;

      :: INTERVA1:def12

      func InterLatt U -> strict non empty LattStr means

      : Def12: the carrier of it = ( IntervalSets U) & for a,b be Element of the carrier of it , a9,b9 be non empty IntervalSet of U st a9 = a & b9 = b holds (the L_join of it . (a,b)) = (a9 _\/_ b9) & (the L_meet of it . (a,b)) = (a9 _/\_ b9);

      existence

      proof

        set B = ( IntervalSets U);

        defpred P[ Element of B, Element of B, Element of B] means ex a9,b9 be non empty IntervalSet of U st a9 = $1 & b9 = $2 & $3 = (a9 _\/_ b9);

        

         A1: for x,y be Element of B holds ex z be Element of B st P[x, y, z]

        proof

          let x,y be Element of B;

          reconsider x9 = x, y9 = y as non empty IntervalSet of U by Def11;

          reconsider z = (x9 _\/_ y9) as Element of B by Def11;

          take z;

          thus thesis;

        end;

        consider B1 be BinOp of B such that

         A2: for x,y be Element of B holds P[x, y, (B1 . (x,y))] from BINOP_1:sch 3( A1);

        defpred R[ Element of B, Element of B, Element of B] means ex a9,b9 be non empty IntervalSet of U st a9 = $1 & b9 = $2 & $3 = (a9 _/\_ b9);

        

         A3: for x,y be Element of B holds ex z be Element of B st R[x, y, z]

        proof

          let x,y be Element of B;

          reconsider x9 = x, y9 = y as non empty IntervalSet of U by Def11;

          reconsider z = (x9 _/\_ y9) as Element of B by Def11;

          take z;

          thus thesis;

        end;

        consider B2 be BinOp of B such that

         A4: for x,y be Element of B holds R[x, y, (B2 . (x,y))] from BINOP_1:sch 3( A3);

        take IT = LattStr (# B, B1, B2 #);

        thus the carrier of IT = ( IntervalSets U);

        let a,b be Element of the carrier of IT, a9,b9 be non empty IntervalSet of U;

        assume

         A5: a9 = a & b9 = b;

        reconsider x = a, y = b as Element of B;

        consider a9,b9 be non empty IntervalSet of U such that

         A6: a9 = x & b9 = y & (B1 . (x,y)) = (a9 _\/_ b9) by A2;

        consider a1,b1 be non empty IntervalSet of U such that

         A7: a1 = x & b1 = y & (B2 . (x,y)) = (a1 _/\_ b1) by A4;

        thus thesis by A6, A7, A5;

      end;

      uniqueness

      proof

        let L1,L2 be strict non empty LattStr such that

         A8: the carrier of L1 = ( IntervalSets U) & for a,b be Element of the carrier of L1, a9,b9 be non empty IntervalSet of U st a9 = a & b9 = b holds (the L_join of L1 . (a,b)) = (a9 _\/_ b9) & (the L_meet of L1 . (a,b)) = (a9 _/\_ b9) and

         A9: the carrier of L2 = ( IntervalSets U) & for a,b be Element of the carrier of L2, a9,b9 be non empty IntervalSet of U st a9 = a & b9 = b holds (the L_join of L2 . (a,b)) = (a9 _\/_ b9) & (the L_meet of L2 . (a,b)) = (a9 _/\_ b9);

        for a,b be Element of L1 holds (the L_join of L1 . (a,b)) = (the L_join of L2 . (a,b))

        proof

          let a,b be Element of L1;

          reconsider a9 = a, b9 = b as non empty IntervalSet of U by A8, Def11;

          (the L_join of L1 . (a,b)) = (a9 _\/_ b9) by A8

          .= (the L_join of L2 . (a,b)) by A9, A8;

          hence thesis;

        end;

        then

         A10: the L_join of L1 = the L_join of L2 by A8, A9, BINOP_1: 2;

        for a,b be Element of L1 holds (the L_meet of L1 . (a,b)) = (the L_meet of L2 . (a,b))

        proof

          let a,b be Element of L1;

          reconsider a9 = a, b9 = b as non empty IntervalSet of U by A8, Def11;

          (the L_meet of L1 . (a,b)) = (a9 _/\_ b9) by A8

          .= (the L_meet of L2 . (a,b)) by A8, A9;

          hence thesis;

        end;

        hence thesis by A8, A9, A10, BINOP_1: 2;

      end;

    end

    registration

      let U be non empty set;

      cluster ( InterLatt U) -> Lattice-like;

      correctness

      proof

        

         A1: ( InterLatt U) is join-commutative

        proof

          for a,b be Element of ( InterLatt U) holds (a "\/" b) = (b "\/" a)

          proof

            let a,b be Element of ( InterLatt U);

            a in the carrier of ( InterLatt U) & b in the carrier of ( InterLatt U);

            then a in ( IntervalSets U) & b in ( IntervalSets U) by Def12;

            then

            reconsider a9 = a, b9 = b as non empty IntervalSet of U by Def11;

            (a "\/" b) = (a9 _\/_ b9) by Def12

            .= (b9 _\/_ a9)

            .= (b "\/" a) by Def12;

            hence thesis;

          end;

          hence thesis;

        end;

        

         A2: ( InterLatt U) is join-associative

        proof

          for a,b,c be Element of ( InterLatt U) holds (a "\/" (b "\/" c)) = ((a "\/" b) "\/" c)

          proof

            let a,b,c be Element of ( InterLatt U);

            a in the carrier of ( InterLatt U) & b in the carrier of ( InterLatt U) & c in the carrier of ( InterLatt U);

            then a in ( IntervalSets U) & b in ( IntervalSets U) & c in ( IntervalSets U) by Def12;

            then

            reconsider a9 = a, b9 = b, c9 = c as non empty IntervalSet of U by Def11;

            reconsider bc = (b9 _\/_ c9) as non empty IntervalSet of U;

            reconsider ab = (a9 _\/_ b9) as non empty IntervalSet of U;

            bc in ( IntervalSets U) & ab in ( IntervalSets U) by Def11;

            then

             A3: bc in the carrier of ( InterLatt U) & ab in the carrier of ( InterLatt U) by Def12;

            (a "\/" (b "\/" c)) = (the L_join of ( InterLatt U) . (a,bc)) by Def12

            .= (a9 _\/_ bc) by Def12, A3

            .= ((a9 _\/_ b9) _\/_ c9) by Th23

            .= (the L_join of ( InterLatt U) . (ab,c9)) by Def12, A3

            .= ((a "\/" b) "\/" c) by Def12;

            hence thesis;

          end;

          hence thesis;

        end;

        

         A4: ( InterLatt U) is meet-absorbing

        proof

          for a,b be Element of ( InterLatt U) holds ((a "/\" b) "\/" b) = b

          proof

            let a,b be Element of ( InterLatt U);

            a in the carrier of ( InterLatt U) & b in the carrier of ( InterLatt U);

            then a in ( IntervalSets U) & b in ( IntervalSets U) by Def12;

            then

            reconsider a9 = a, b9 = b as non empty IntervalSet of U by Def11;

            reconsider ab = (a9 _/\_ b9) as non empty IntervalSet of U;

            ab in ( IntervalSets U) by Def11;

            then

             A5: ab in the carrier of ( InterLatt U) by Def12;

            ((a "/\" b) "\/" b) = (the L_join of ( InterLatt U) . (ab,b)) by Def12

            .= (ab _\/_ b9) by Def12, A5

            .= b by Th36;

            hence thesis;

          end;

          hence thesis;

        end;

        

         A6: ( InterLatt U) is meet-associative

        proof

          for a,b,c be Element of ( InterLatt U) holds (a "/\" (b "/\" c)) = ((a "/\" b) "/\" c)

          proof

            let a,b,c be Element of ( InterLatt U);

            a in the carrier of ( InterLatt U) & b in the carrier of ( InterLatt U) & c in the carrier of ( InterLatt U);

            then a in ( IntervalSets U) & b in ( IntervalSets U) & c in ( IntervalSets U) by Def12;

            then

            reconsider a9 = a, b9 = b, c9 = c as non empty IntervalSet of U by Def11;

            reconsider bc = (b9 _/\_ c9), ab = (a9 _/\_ b9) as non empty IntervalSet of U;

            bc in ( IntervalSets U) & ab in ( IntervalSets U) by Def11;

            then

             A7: bc in the carrier of ( InterLatt U) & ab in the carrier of ( InterLatt U) by Def12;

            (a "/\" (b "/\" c)) = (the L_meet of ( InterLatt U) . (a,bc)) by Def12

            .= (a9 _/\_ bc) by Def12, A7

            .= ((a9 _/\_ b9) _/\_ c9) by Th24

            .= (the L_meet of ( InterLatt U) . (ab,c9)) by Def12, A7

            .= ((a "/\" b) "/\" c) by Def12;

            hence thesis;

          end;

          hence thesis;

        end;

        

         A8: ( InterLatt U) is join-absorbing

        proof

          for a,b be Element of the carrier of ( InterLatt U) holds (a "/\" (a "\/" b)) = a

          proof

            let a,b be Element of the carrier of ( InterLatt U);

            a in the carrier of ( InterLatt U) & b in the carrier of ( InterLatt U);

            then a in ( IntervalSets U) & b in ( IntervalSets U) by Def12;

            then

            reconsider a9 = a, b9 = b as non empty IntervalSet of U by Def11;

            reconsider ab = (a9 _\/_ b9) as non empty IntervalSet of U;

            ab in ( IntervalSets U) by Def11;

            then

             A9: ab in the carrier of ( InterLatt U) by Def12;

            (a "/\" (a "\/" b)) = (the L_meet of ( InterLatt U) . (a9,(a9 _\/_ b9))) by Def12

            .= (a9 _/\_ ab) by Def12, A9

            .= a by Th35;

            hence thesis;

          end;

          hence thesis;

        end;

        ( InterLatt U) is meet-commutative

        proof

          for a,b be Element of the carrier of ( InterLatt U) holds (a "/\" b) = (b "/\" a)

          proof

            let a,b be Element of the carrier of ( InterLatt U);

            a in the carrier of ( InterLatt U) & b in the carrier of ( InterLatt U);

            then a in ( IntervalSets U) & b in ( IntervalSets U) by Def12;

            then

            reconsider a9 = a, b9 = b as non empty IntervalSet of U by Def11;

            (a9 _/\_ b9) = (b9 _/\_ a9);

            

            then (the L_meet of ( InterLatt U) . (a,b)) = (b9 _/\_ a9) by Def12

            .= (the L_meet of ( InterLatt U) . (b,a)) by Def12;

            hence thesis;

          end;

          hence thesis;

        end;

        hence thesis by A1, A2, A4, A6, A8;

      end;

    end

    definition

      let X be Tolerance_Space;

      :: INTERVA1:def13

      mode RoughSet of X -> Element of [:( bool the carrier of X), ( bool the carrier of X):] means

      : Def13: not contradiction;

      existence ;

    end

    theorem :: INTERVA1:55

    

     Th55: for X be Tolerance_Space, A be RoughSet of X holds ex B,C be Subset of X st A = [B, C]

    proof

      let X be Tolerance_Space, A be RoughSet of X;

      consider A1,A2 be object such that

       A1: A1 in ( bool the carrier of X) & A2 in ( bool the carrier of X) & A = [A1, A2] by ZFMISC_1:def 2;

      reconsider A1, A2 as Subset of X by A1;

      take A1, A2;

      thus thesis by A1;

    end;

    definition

      let X be Tolerance_Space, A be Subset of X;

      :: INTERVA1:def14

      func RS A -> RoughSet of X equals [( LAp A), ( UAp A)];

      coherence

      proof

         [( LAp A), ( UAp A)] in [:( bool the carrier of X), ( bool the carrier of X):] by ZFMISC_1: 87;

        hence thesis by Def13;

      end;

    end

    definition

      let X be Tolerance_Space, A be RoughSet of X;

      :: INTERVA1:def15

      func LAp A -> Subset of X equals (A `1 );

      coherence

      proof

        consider A9,B9 be Subset of X such that

         A1: A = [A9, B9] by Th55;

        thus thesis by A1;

      end;

      :: INTERVA1:def16

      func UAp A -> Subset of X equals (A `2 );

      coherence

      proof

        consider A9,B9 be Subset of X such that

         A2: A = [A9, B9] by Th55;

        thus thesis by A2;

      end;

    end

    definition

      let X be Tolerance_Space;

      let A,B be RoughSet of X;

      :: original: =

      redefine

      :: INTERVA1:def17

      pred A = B means ( LAp A) = ( LAp B) & ( UAp A) = ( UAp B);

      compatibility

      proof

        thus A = B implies ( LAp A) = ( LAp B) & ( UAp A) = ( UAp B);

        assume

         A1: ( LAp A) = ( LAp B) & ( UAp A) = ( UAp B);

        consider A1,B1 be Subset of X such that

         A2: A = [A1, B1] by Th55;

        consider A2,B2 be Subset of X such that

         A3: B = [A2, B2] by Th55;

        ( LAp A) = A1 by A2;

        then

         A4: A1 = A2 by A1, A3;

        ( UAp A) = B1 by A2;

        then B1 = B2 by A1, A3;

        hence A = B by A2, A4, A3;

      end;

    end

    definition

      let X be Tolerance_Space;

      let A,B be RoughSet of X;

      :: INTERVA1:def18

      func A _\/_ B -> RoughSet of X equals [(( LAp A) \/ ( LAp B)), (( UAp A) \/ ( UAp B))];

      coherence

      proof

         [(( LAp A) \/ ( LAp B)), (( UAp A) \/ ( UAp B))] in [:( bool the carrier of X), ( bool the carrier of X):] by ZFMISC_1: 87;

        hence thesis by Def13;

      end;

      :: INTERVA1:def19

      func A _/\_ B -> RoughSet of X equals [(( LAp A) /\ ( LAp B)), (( UAp A) /\ ( UAp B))];

      coherence

      proof

         [(( LAp A) /\ ( LAp B)), (( UAp A) /\ ( UAp B))] in [:( bool the carrier of X), ( bool the carrier of X):] by ZFMISC_1: 87;

        hence thesis by Def13;

      end;

    end

    reserve X for Tolerance_Space,

A,B,C for RoughSet of X;

    theorem :: INTERVA1:56

    ( LAp (A _\/_ B)) = (( LAp A) \/ ( LAp B));

    theorem :: INTERVA1:57

    ( UAp (A _\/_ B)) = (( UAp A) \/ ( UAp B));

    theorem :: INTERVA1:58

    ( LAp (A _/\_ B)) = (( LAp A) /\ ( LAp B));

    theorem :: INTERVA1:59

    ( UAp (A _/\_ B)) = (( UAp A) /\ ( UAp B));

    theorem :: INTERVA1:60

    (A _\/_ A) = A;

    theorem :: INTERVA1:61

    

     Th61: (A _/\_ A) = A;

    theorem :: INTERVA1:62

    (A _\/_ B) = (B _\/_ A);

    theorem :: INTERVA1:63

    (A _/\_ B) = (B _/\_ A);

    theorem :: INTERVA1:64

    

     Th64: ((A _\/_ B) _\/_ C) = (A _\/_ (B _\/_ C)) by XBOOLE_1: 4;

    theorem :: INTERVA1:65

    

     Th65: ((A _/\_ B) _/\_ C) = (A _/\_ (B _/\_ C)) by XBOOLE_1: 16;

    theorem :: INTERVA1:66

    

     Th66: (A _/\_ (B _\/_ C)) = ((A _/\_ B) _\/_ (A _/\_ C)) by XBOOLE_1: 23;

    theorem :: INTERVA1:67

    

     Th67: (A _\/_ (A _/\_ B)) = A by XBOOLE_1: 22;

    theorem :: INTERVA1:68

    (A _/\_ (A _\/_ B)) = A by XBOOLE_1: 21;

    begin

    definition

      let X;

      :: INTERVA1:def20

      func RoughSets X -> set means

      : Def20: for x be set holds x in it iff x is RoughSet of X;

      existence

      proof

        defpred P[ object] means $1 is RoughSet of X;

        consider F be set such that

         A1: for x be object holds x in F iff x in [:( bool the carrier of X), ( bool the carrier of X):] & P[x] from XBOOLE_0:sch 1;

        take F;

        let x be set;

        thus x in F implies x is RoughSet of X by A1;

        assume x is RoughSet of X;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let F1,F2 be set such that

         A2: (for x be set holds x in F1 iff x is RoughSet of X) & (for x be set holds x in F2 iff x is RoughSet of X);

        for x be object holds x in F1 iff x in F2 by A2;

        hence thesis by TARSKI: 2;

      end;

    end

    registration

      let X;

      cluster ( RoughSets X) -> non empty;

      coherence

      proof

        set A = the RoughSet of X;

        A in ( RoughSets X) by Def20;

        hence thesis;

      end;

    end

    definition

      let X;

      let R be Element of ( RoughSets X);

      :: INTERVA1:def21

      func @ R -> RoughSet of X equals R;

      coherence by Def20;

    end

    definition

      let X;

      let R be RoughSet of X;

      :: INTERVA1:def22

      func R @ -> Element of ( RoughSets X) equals R;

      coherence by Def20;

    end

    definition

      let X;

      :: INTERVA1:def23

      func RSLattice X -> strict LattStr means

      : Def23: the carrier of it = ( RoughSets X) & for A,B be Element of ( RoughSets X), A9,B9 be RoughSet of X st A = A9 & B = B9 holds (the L_join of it . (A,B)) = (A9 _\/_ B9) & (the L_meet of it . (A,B)) = (A9 _/\_ B9);

      existence

      proof

        deffunc U( Element of ( RoughSets X), Element of ( RoughSets X)) = ((( @ $1) _\/_ ( @ $2)) @ );

        consider j be BinOp of ( RoughSets X) such that

         A1: for x,y be Element of ( RoughSets X) holds (j . (x,y)) = U(x,y) from BINOP_1:sch 4;

        deffunc W( Element of ( RoughSets X), Element of ( RoughSets X)) = ((( @ $1) _/\_ ( @ $2)) @ );

        consider m be BinOp of ( RoughSets X) such that

         A2: for x,y be Element of ( RoughSets X) holds (m . (x,y)) = W(x,y) from BINOP_1:sch 4;

        take IT = LattStr (# ( RoughSets X), j, m #);

        thus the carrier of IT = ( RoughSets X);

        let A,B be Element of ( RoughSets X), A9,B9 be RoughSet of X;

        assume

         A3: A = A9 & B = B9;

        

        thus (the L_join of IT . (A,B)) = U(A,B) by A1

        .= (A9 _\/_ B9) by A3;

        

        thus (the L_meet of IT . (A,B)) = W(A,B) by A2

        .= (A9 _/\_ B9) by A3;

      end;

      uniqueness

      proof

        let A1,A2 be strict LattStr such that

         A4: the carrier of A1 = ( RoughSets X) & for A,B be Element of ( RoughSets X), A9,B9 be RoughSet of X st A = A9 & B = B9 holds (the L_join of A1 . (A,B)) = (A9 _\/_ B9) & (the L_meet of A1 . (A,B)) = (A9 _/\_ B9) and

         A5: the carrier of A2 = ( RoughSets X) & for A,B be Element of ( RoughSets X), A9,B9 be RoughSet of X st A = A9 & B = B9 holds (the L_join of A2 . (A,B)) = (A9 _\/_ B9) & (the L_meet of A2 . (A,B)) = (A9 _/\_ B9);

        reconsider a3 = the L_meet of A1, a4 = the L_meet of A2, a1 = the L_join of A1, a2 = the L_join of A2 as BinOp of ( RoughSets X) by A4, A5;

        now

          let x,y be Element of ( RoughSets X);

          

          thus (a1 . (x,y)) = (( @ x) _\/_ ( @ y)) by A4

          .= (a2 . (x,y)) by A5;

        end;

        then

         A6: a1 = a2 by BINOP_1: 2;

        now

          let x,y be Element of ( RoughSets X);

          

          thus (a3 . (x,y)) = (( @ x) _/\_ ( @ y)) by A4

          .= (a4 . (x,y)) by A5;

        end;

        hence thesis by A4, A5, A6, BINOP_1: 2;

      end;

    end

    registration

      let X;

      cluster ( RSLattice X) -> non empty;

      coherence

      proof

        the carrier of ( RSLattice X) = ( RoughSets X) by Def23;

        hence thesis;

      end;

    end

    

     Lm6: for a,b be Element of ( RSLattice X) holds (a "\/" b) = (b "\/" a)

    proof

      set G = ( RSLattice X);

      let a,b be Element of G;

      reconsider a1 = a, b1 = b as Element of ( RoughSets X) by Def23;

      reconsider a9 = a1, b9 = b1 as RoughSet of X by Def20;

      (a "\/" b) = (a9 _\/_ b9) by Def23

      .= (b9 _\/_ a9)

      .= (b "\/" a) by Def23;

      hence thesis;

    end;

    

     Lm7: for a,b,c be Element of ( RSLattice X) holds (a "\/" (b "\/" c)) = ((a "\/" b) "\/" c)

    proof

      let a,b,c be Element of ( RSLattice X);

      reconsider a1 = a, b1 = b, c1 = c as Element of ( RoughSets X) by Def23;

      reconsider a9 = a1, b9 = b1, c9 = c1 as RoughSet of X by Def20;

      set G = ( RSLattice X);

      

       A1: (b9 _\/_ c9) is Element of ( RoughSets X) by Def20;

      

       A2: (a9 _\/_ b9) is Element of ( RoughSets X) by Def20;

      (a "\/" (b "\/" c)) = (the L_join of G . (a,(b9 _\/_ c9))) by Def23

      .= (a9 _\/_ (b9 _\/_ c9)) by Def23, A1

      .= ((a9 _\/_ b9) _\/_ c9) by Th64

      .= (the L_join of G . ((a9 _\/_ b9),c1)) by Def23, A2

      .= ((a "\/" b) "\/" c) by Def23;

      hence thesis;

    end;

    reserve K,L,M for Element of ( RoughSets X);

    

     Lm8: (the L_join of ( RSLattice X) . ((the L_meet of ( RSLattice X) . (K,L)),L)) = L

    proof

      reconsider K9 = K, L9 = L as RoughSet of X by Def20;

      

       A1: (K9 _/\_ L9) is Element of ( RoughSets X) by Def20;

      

      thus (the L_join of ( RSLattice X) . ((the L_meet of ( RSLattice X) . (K,L)),L)) = (the L_join of ( RSLattice X) . ((K9 _/\_ L9),L)) by Def23

      .= ((K9 _/\_ L9) _\/_ L9) by Def23, A1

      .= (L9 _\/_ (L9 _/\_ K9))

      .= L by Th67;

    end;

    

     Lm9: for a,b be Element of ( RSLattice X) holds ((a "/\" b) "\/" b) = b

    proof

      let a,b be Element of ( RSLattice X);

      set G = ( RSLattice X);

      reconsider a1 = a, b1 = b as Element of ( RoughSets X) by Def23;

      

      thus ((a "/\" b) "\/" b) = (the L_join of G . ((the L_meet of G . (a1,b1)),b1))

      .= b by Lm8;

    end;

    

     Lm10: for a,b be Element of ( RSLattice X) holds (a "/\" b) = (b "/\" a)

    proof

      let a,b be Element of ( RSLattice X);

      reconsider a1 = a, b1 = b as Element of ( RoughSets X) by Def23;

      reconsider a9 = a1, b9 = b1 as RoughSet of X by Def20;

      (a "/\" b) = (a9 _/\_ b9) by Def23

      .= (b9 _/\_ a9)

      .= (b "/\" a) by Def23;

      hence thesis;

    end;

    

     Lm11: for a,b,c be Element of ( RSLattice X) holds (a "/\" (b "/\" c)) = ((a "/\" b) "/\" c)

    proof

      let a,b,c be Element of ( RSLattice X);

      reconsider a1 = a, b1 = b, c1 = c as Element of ( RoughSets X) by Def23;

      reconsider a9 = a1, b9 = b1, c9 = c1 as RoughSet of X by Def20;

      set G = ( RSLattice X);

      

       A1: (b9 _/\_ c9) is Element of ( RoughSets X) by Def20;

      

       A2: (a9 _/\_ b9) is Element of ( RoughSets X) by Def20;

      (a "/\" (b "/\" c)) = (the L_meet of G . (a1,(b9 _/\_ c9))) by Def23

      .= (a9 _/\_ (b9 _/\_ c9)) by Def23, A1

      .= ((a9 _/\_ b9) _/\_ c9) by Th65

      .= (the L_meet of G . ((a9 _/\_ b9),c1)) by Def23, A2

      .= ((a "/\" b) "/\" c) by Def23;

      hence thesis;

    end;

    

     Lm12: (the L_meet of ( RSLattice X) . (K,(the L_join of ( RSLattice X) . (L,M)))) = (the L_join of ( RSLattice X) . ((the L_meet of ( RSLattice X) . (K,L)),(the L_meet of ( RSLattice X) . (K,M))))

    proof

      set G = ( RSLattice X);

      reconsider K9 = K, L9 = L, M9 = M as RoughSet of X by Def20;

      

       A1: (L9 _\/_ M9) is Element of ( RoughSets X) by Def20;

      

       A2: (K9 _/\_ L9) is Element of ( RoughSets X) by Def20;

      

       A3: (K9 _/\_ M9) is Element of ( RoughSets X) by Def20;

      (the L_meet of G . (K,(the L_join of G . (L,M)))) = (the L_meet of G . (K,(L9 _\/_ M9))) by Def23

      .= (K9 _/\_ (L9 _\/_ M9)) by Def23, A1

      .= ((K9 _/\_ L9) _\/_ (K9 _/\_ M9)) by Th66

      .= (the L_join of G . ((K9 _/\_ L9),(K9 _/\_ M9))) by Def23, A2, A3

      .= (the L_join of G . ((the L_meet of G . (K,L)),(K9 _/\_ M9))) by Def23

      .= (the L_join of G . ((the L_meet of G . (K,L)),(the L_meet of G . (K,M)))) by Def23;

      hence thesis;

    end;

    

     Lm13: for a,b be Element of ( RSLattice X) holds (a "/\" (a "\/" b)) = a

    proof

      let a,b be Element of ( RSLattice X);

      set G = ( RSLattice X);

      reconsider a1 = a, b1 = b as Element of ( RoughSets X) by Def23;

      reconsider a9 = a1 as RoughSet of X by Def20;

      

      thus (a "/\" (a "\/" b)) = (the L_join of G . ((the L_meet of G . (a1,a1)),(the L_meet of G . (a1,b1)))) by Lm12

      .= (the L_join of G . ((a9 _/\_ a9),(the L_meet of G . (a1,b1)))) by Def23

      .= (a "\/" (a "/\" b)) by Th61

      .= ((a "/\" b) "\/" a) by Lm6

      .= ((b "/\" a) "\/" a) by Lm10

      .= a by Lm9;

    end;

    registration

      let X;

      cluster ( RSLattice X) -> Lattice-like;

      coherence

      proof

        set G = ( RSLattice X);

        thus for u,v be Element of G holds (u "\/" v) = (v "\/" u) by Lm6;

        thus for u,v,w be Element of G holds (u "\/" (v "\/" w)) = ((u "\/" v) "\/" w) by Lm7;

        thus for u,v be Element of G holds ((u "/\" v) "\/" v) = v by Lm9;

        thus for u,v be Element of G holds (u "/\" v) = (v "/\" u) by Lm10;

        thus for u,v,w be Element of G holds (u "/\" (v "/\" w)) = ((u "/\" v) "/\" w) by Lm11;

        let u,v be Element of G;

        thus (u "/\" (u "\/" v)) = u by Lm13;

      end;

    end

    registration

      let X;

      cluster ( RSLattice X) -> distributive;

      coherence

      proof

        let u,v,w be Element of ( RSLattice X);

        reconsider K = u, L = v, M = w as Element of ( RoughSets X) by Def23;

        

        thus (u "/\" (v "\/" w)) = (the L_join of ( RSLattice X) . ((the L_meet of ( RSLattice X) . (K,L)),(the L_meet of ( RSLattice X) . (K,M)))) by Lm12

        .= ((u "/\" v) "\/" (u "/\" w));

      end;

    end

    definition

      let X;

      :: INTERVA1:def24

      func ERS X -> RoughSet of X equals [ {} , {} ];

      coherence

      proof

        reconsider A = {} as Subset of X by XBOOLE_1: 2;

        A = ( {} X);

        then

         A1: ( LAp A) = {} & ( UAp A) = {} by ROUGHS_1: 18, ROUGHS_1: 19;

         [( LAp A), ( UAp A)] in [:( bool the carrier of X), ( bool the carrier of X):] by ZFMISC_1: 87;

        hence thesis by Def13, A1;

      end;

    end

    

     Lm14: ( ERS X) in ( RoughSets X) by Def20;

    theorem :: INTERVA1:69

    

     Th69: for A be RoughSet of X holds (( ERS X) _\/_ A) = A;

    definition

      let X;

      :: INTERVA1:def25

      func TRS X -> RoughSet of X equals [( [#] X), ( [#] X)];

      coherence

      proof

        reconsider A = ( [#] X) as Subset of X;

        

         A1: ( LAp A) = ( [#] X) & ( UAp A) = ( [#] X) by ROUGHS_1: 20, ROUGHS_1: 21;

         [( LAp A), ( UAp A)] in [:( bool the carrier of X), ( bool the carrier of X):] by ZFMISC_1: 87;

        hence thesis by Def13, A1;

      end;

    end

    

     Lm15: ( TRS X) in ( RoughSets X) by Def20;

    theorem :: INTERVA1:70

    

     Th70: for A be RoughSet of X holds (( TRS X) _/\_ A) = A by XBOOLE_1: 28;

    registration

      let X;

      cluster ( RSLattice X) -> bounded;

      coherence

      proof

        thus ( RSLattice X) is lower-bounded

        proof

          reconsider E = ( ERS X) as Element of ( RoughSets X) by Lm14;

          reconsider e = E as Element of ( RSLattice X) by Def23;

          take e;

          let u be Element of ( RSLattice X);

          reconsider K = u as Element of ( RoughSets X) by Def23;

          reconsider E9 = E, K9 = K as RoughSet of X by Def20;

          (e "\/" u) = (E9 _\/_ K9) by Def23

          .= u by Th69;

          then (e "/\" u) = e & (u "/\" e) = e by LATTICES:def 9;

          hence thesis;

        end;

        thus ( RSLattice X) is upper-bounded

        proof

          reconsider E = ( TRS X) as Element of ( RoughSets X) by Lm15;

          reconsider e = E as Element of ( RSLattice X) by Def23;

          take e;

          let u be Element of ( RSLattice X);

          reconsider K = u as Element of ( RoughSets X) by Def23;

          reconsider E9 = E, K9 = K as RoughSet of X by Def20;

          (e "/\" u) = (E9 _/\_ K9) by Def23

          .= u by Th70;

          then (e "\/" u) = e & (u "\/" e) = e by LATTICES:def 8;

          hence thesis;

        end;

      end;

    end

    theorem :: INTERVA1:71

    

     Th71: for X be Tolerance_Space, A,B be Element of ( RSLattice X), A9,B9 be RoughSet of X st A = A9 & B = B9 holds A [= B iff ( LAp A9) c= ( LAp B9) & ( UAp A9) c= ( UAp B9)

    proof

      let X be Tolerance_Space, A,B be Element of ( RSLattice X), A9,B9 be RoughSet of X;

      assume

       A1: A = A9 & B = B9;

      

       A2: A is Element of ( RoughSets X) & B is Element of ( RoughSets X) by Def23;

      thus A [= B implies ( LAp A9) c= ( LAp B9) & ( UAp A9) c= ( UAp B9)

      proof

        assume A [= B;

        then (A "\/" B) = B;

        then (A9 _\/_ B9) = B9 by A1, Def23, A2;

        then (( LAp A9) \/ ( LAp B9)) = ( LAp B9) & (( UAp A9) \/ ( UAp B9)) = ( UAp B9);

        hence thesis by XBOOLE_1: 11;

      end;

      assume ( LAp A9) c= ( LAp B9) & ( UAp A9) c= ( UAp B9);

      then (( LAp A9) \/ ( LAp B9)) = ( LAp B9) & (( UAp A9) \/ ( UAp B9)) = ( UAp B9) by XBOOLE_1: 12;

      then ( LAp (A9 _\/_ B9)) = ( LAp B9) & ( UAp (A9 _\/_ B9)) = ( UAp B9);

      then

       A3: (A9 _\/_ B9) = B9;

      reconsider A1 = A, B1 = B as Element of ( RoughSets X) by Def23;

      reconsider A9 = A1, B9 = B1 as RoughSet of X by Def20;

      (A9 _\/_ B9) = (A "\/" B) by Def23;

      hence thesis by A3, A1;

    end;

    

     Lm16: ( RSLattice X) is complete

    proof

      let Y be Subset of ( RSLattice X);

      ex a be Element of ( RSLattice X) st a is_less_than Y & for b be Element of ( RSLattice X) st b is_less_than Y holds b [= a

      proof

        per cases ;

          suppose

           A1: Y is empty;

          take a = ( Top ( RSLattice X));

          for q be Element of ( RSLattice X) st q in Y holds a [= q by A1;

          hence a is_less_than Y;

          let b be Element of ( RSLattice X);

          assume b is_less_than Y;

          thus b [= a by LATTICES: 19;

        end;

          suppose

           A2: Y is non empty;

          set A1 = { ( LAp a1) where a1 be RoughSet of X : a1 in Y };

          set A2 = { ( UAp a1) where a1 be RoughSet of X : a1 in Y };

          set a9 = [( meet A1), ( meet A2)];

          consider f be object such that

           A3: f in Y by A2;

          Y is Subset of ( RoughSets X) by Def23;

          then

          reconsider f as RoughSet of X by A3, Def20;

          

           A4: ( LAp f) in A1 by A3;

          then

           A5: A1 <> {} ;

          consider g be object such that

           A6: g in Y by A2;

          Y is Subset of ( RoughSets X) by Def23;

          then

          reconsider g as RoughSet of X by A6, Def20;

          ( UAp g) in A2 by A6;

          then

           A7: A2 <> {} ;

          

           A8: ( meet A1) c= the carrier of X

          proof

            let x be object;

            assume x in ( meet A1);

            then

             A9: for Z be set holds Z in A1 implies x in Z by SETFAM_1:def 1;

            consider c be set such that

             A10: c in A1 by A4;

            consider c9 be RoughSet of X such that

             A11: c = ( LAp c9) & c9 in Y by A10;

            

             A12: c in ( bool the carrier of X) by A11;

            x in c by A10, A9;

            hence thesis by A12;

          end;

          a9 is RoughSet of X

          proof

            ( meet A2) c= the carrier of X

            proof

              let x be object;

              assume x in ( meet A2);

              then

               A13: for Z be set holds Z in A2 implies x in Z by SETFAM_1:def 1;

              consider c be object such that

               A14: c in A2 by A7, XBOOLE_0:def 1;

              consider c9 be RoughSet of X such that

               A15: c = ( UAp c9) & c9 in Y by A14;

              reconsider c as set by TARSKI: 1;

              

               A16: c c= the carrier of X by A15;

              x in c by A14, A13;

              hence thesis by A16;

            end;

            then [( meet A1), ( meet A2)] in [:( bool the carrier of X), ( bool the carrier of X):] by A8, ZFMISC_1: 87;

            hence thesis by Def13;

          end;

          then

          reconsider a9 as RoughSet of X;

          a9 in ( RoughSets X) by Def20;

          then

          reconsider a = a9 as Element of ( RSLattice X) by Def23;

          take a;

          thus a is_less_than Y

          proof

            let q be Element of ( RSLattice X);

            assume

             A17: q in Y;

            q in the carrier of ( RSLattice X);

            then q in ( RoughSets X) by Def23;

            then

            reconsider q9 = q as RoughSet of X by Def20;

            consider q1,q2 be Subset of X such that

             A18: q9 = [q1, q2] by Th55;

            

             A19: q1 = ( LAp q9) by A18;

            then

             A20: q1 in A1 by A17;

            ( meet A1) c= ( LAp q9) by A19, A20, SETFAM_1:def 1;

            then

             A21: ( LAp a9) c= ( LAp q9);

            

             A22: ( UAp a9) = ( meet A2);

            

             A23: q2 = ( UAp q9) by A18;

            then

             A24: q2 in A2 by A17;

            ( meet A2) c= ( UAp q9) by A23, A24, SETFAM_1:def 1;

            hence a [= q by A21, Th71, A22;

          end;

          thus for b be Element of ( RSLattice X) st b is_less_than Y holds b [= a

          proof

            let b be Element of ( RSLattice X);

            assume

             A25: b is_less_than Y;

            b is Element of ( RoughSets X) by Def23;

            then

            reconsider b9 = b as RoughSet of X by Def20;

            reconsider a9 = a as RoughSet of X;

            

             A26: for q be Element of ( RSLattice X) st q in Y holds b [= q by A25;

            for Z1 be set st Z1 in A1 holds ( LAp b9) c= Z1

            proof

              let Z1 be set;

              assume Z1 in A1;

              then

              consider c1 be RoughSet of X such that

               A27: Z1 = ( LAp c1) & c1 in Y;

              reconsider c19 = c1 as Element of ( RSLattice X) by A27;

              b [= c19 by A25, A27;

              hence thesis by A27, Th71;

            end;

            then

             A28: ( LAp b9) c= ( meet A1) by A5, SETFAM_1: 5;

            

             A29: ( LAp b9) c= ( LAp a9) by A28;

            for Z1 be set st Z1 in A2 holds ( UAp b9) c= Z1

            proof

              let Z1 be set;

              assume Z1 in A2;

              then

              consider c2 be RoughSet of X such that

               A30: Z1 = ( UAp c2) & c2 in Y;

              reconsider c29 = c2 as Element of ( RSLattice X) by A30;

              b [= c29 by A26, A30;

              hence thesis by A30, Th71;

            end;

            then

             A31: ( UAp b9) c= ( meet A2) by A7, SETFAM_1: 5;

            ( UAp b9) c= ( UAp a9) by A31;

            hence thesis by A29, Th71;

          end;

        end;

      end;

      hence thesis;

    end;

    registration

      let X;

      cluster ( RSLattice X) -> complete;

      coherence by Lm16;

    end