setlim_2.miz



    begin

    reserve n,m,k for Nat,

x,X for set,

A for Subset of X,

A1,A2 for SetSequence of X;

    theorem :: SETLIM_2:1

    

     Th1: (( inferior_setsequence A1) . n) = ( Intersection (A1 ^\ n))

    proof

      reconsider Y = { (A1 . k) : n <= k } as Subset-Family of X by SETLIM_1: 28;

      (( inferior_setsequence A1) . n) = ( meet Y) by SETLIM_1:def 2

      .= ( meet ( rng (A1 ^\ n))) by SETLIM_1: 6;

      hence thesis by SETLIM_1: 8;

    end;

    theorem :: SETLIM_2:2

    

     Th2: (( superior_setsequence A1) . n) = ( Union (A1 ^\ n))

    proof

      reconsider Y = { (A1 . k) : n <= k } as Subset-Family of X by SETLIM_1: 28;

      (( superior_setsequence A1) . n) = ( union Y) by SETLIM_1:def 3

      .= ( union ( rng (A1 ^\ n))) by SETLIM_1: 6;

      hence thesis by CARD_3:def 4;

    end;

    definition

      let X;

      let A1,A2 be SetSequence of X;

      :: SETLIM_2:def1

      func A1 (/\) A2 -> SetSequence of X means

      : Def1: for n holds (it . n) = ((A1 . n) /\ (A2 . n));

      existence

      proof

        deffunc F( Nat) = ((A1 . $1) /\ (A2 . $1));

        consider f be SetSequence of X such that

         A1: for n be Element of NAT holds (f . n) = F(n) from FUNCT_2:sch 4;

        take f;

        let n;

        n in NAT by ORDINAL1:def 12;

        then (f . n) = F(n) by A1;

        hence thesis;

      end;

      uniqueness

      proof

        let A3 be SetSequence of X, A4 be SetSequence of X such that

         A2: for n holds (A3 . n) = ((A1 . n) /\ (A2 . n)) and

         A3: for n holds (A4 . n) = ((A1 . n) /\ (A2 . n));

        let n be Element of NAT ;

        

        thus (A3 . n) = ((A1 . n) /\ (A2 . n)) by A2

        .= (A4 . n) by A3;

      end;

      commutativity ;

      :: SETLIM_2:def2

      func A1 (\/) A2 -> SetSequence of X means

      : Def2: for n holds (it . n) = ((A1 . n) \/ (A2 . n));

      existence

      proof

        deffunc F( Nat) = ((A1 . $1) \/ (A2 . $1));

        consider f be SetSequence of X such that

         A4: for n be Element of NAT holds (f . n) = F(n) from FUNCT_2:sch 4;

        take f;

        let n;

        n in NAT by ORDINAL1:def 12;

        then (f . n) = F(n) by A4;

        hence thesis;

      end;

      uniqueness

      proof

        let A3 be SetSequence of X, A4 be SetSequence of X such that

         A5: for n holds (A3 . n) = ((A1 . n) \/ (A2 . n)) and

         A6: for n holds (A4 . n) = ((A1 . n) \/ (A2 . n));

        let n be Element of NAT ;

        

        thus (A3 . n) = ((A1 . n) \/ (A2 . n)) by A5

        .= (A4 . n) by A6;

      end;

      commutativity ;

      :: SETLIM_2:def3

      func A1 (\) A2 -> SetSequence of X means

      : Def3: for n holds (it . n) = ((A1 . n) \ (A2 . n));

      existence

      proof

        deffunc F( Nat) = ((A1 . $1) \ (A2 . $1));

        consider f be SetSequence of X such that

         A7: for n be Element of NAT holds (f . n) = F(n) from FUNCT_2:sch 4;

        take f;

        let n;

        n in NAT by ORDINAL1:def 12;

        then (f . n) = F(n) by A7;

        hence thesis;

      end;

      uniqueness

      proof

        let A3 be SetSequence of X, A4 be SetSequence of X such that

         A8: for n holds (A3 . n) = ((A1 . n) \ (A2 . n)) and

         A9: for n holds (A4 . n) = ((A1 . n) \ (A2 . n));

        let n be Element of NAT ;

        

        thus (A3 . n) = ((A1 . n) \ (A2 . n)) by A8

        .= (A4 . n) by A9;

      end;

      :: SETLIM_2:def4

      func A1 (\+\) A2 -> SetSequence of X means

      : Def4: for n holds (it . n) = ((A1 . n) \+\ (A2 . n));

      existence

      proof

        deffunc F( Nat) = ((A1 . $1) \+\ (A2 . $1));

        consider f be SetSequence of X such that

         A10: for n be Element of NAT holds (f . n) = F(n) from FUNCT_2:sch 4;

        take f;

        let n;

        n in NAT by ORDINAL1:def 12;

        then (f . n) = F(n) by A10;

        hence thesis;

      end;

      uniqueness

      proof

        let A3 be SetSequence of X, A4 be SetSequence of X such that

         A11: for n holds (A3 . n) = ((A1 . n) \+\ (A2 . n)) and

         A12: for n holds (A4 . n) = ((A1 . n) \+\ (A2 . n));

        let n be Element of NAT ;

        

        thus (A3 . n) = ((A1 . n) \+\ (A2 . n)) by A11

        .= (A4 . n) by A12;

      end;

      commutativity ;

    end

    theorem :: SETLIM_2:3

    

     Th3: (A1 (\+\) A2) = ((A1 (\) A2) (\/) (A2 (\) A1))

    proof

      let n be Element of NAT ;

      

      thus ((A1 (\+\) A2) . n) = ((A1 . n) \+\ (A2 . n)) by Def4

      .= (((A1 (\) A2) . n) \/ ((A2 . n) \ (A1 . n))) by Def3

      .= (((A1 (\) A2) . n) \/ ((A2 (\) A1) . n)) by Def3

      .= (((A1 (\) A2) (\/) (A2 (\) A1)) . n) by Def2;

    end;

    theorem :: SETLIM_2:4

    

     Th4: ((A1 (/\) A2) ^\ k) = ((A1 ^\ k) (/\) (A2 ^\ k))

    proof

      let n be Element of NAT ;

      

      thus (((A1 (/\) A2) ^\ k) . n) = ((A1 (/\) A2) . (n + k)) by NAT_1:def 3

      .= ((A1 . (n + k)) /\ (A2 . (n + k))) by Def1

      .= (((A1 ^\ k) . n) /\ (A2 . (n + k))) by NAT_1:def 3

      .= (((A1 ^\ k) . n) /\ ((A2 ^\ k) . n)) by NAT_1:def 3

      .= (((A1 ^\ k) (/\) (A2 ^\ k)) . n) by Def1;

    end;

    theorem :: SETLIM_2:5

    

     Th5: ((A1 (\/) A2) ^\ k) = ((A1 ^\ k) (\/) (A2 ^\ k))

    proof

      let n be Element of NAT ;

      

      thus (((A1 (\/) A2) ^\ k) . n) = ((A1 (\/) A2) . (n + k)) by NAT_1:def 3

      .= ((A1 . (n + k)) \/ (A2 . (n + k))) by Def2

      .= (((A1 ^\ k) . n) \/ (A2 . (n + k))) by NAT_1:def 3

      .= (((A1 ^\ k) . n) \/ ((A2 ^\ k) . n)) by NAT_1:def 3

      .= (((A1 ^\ k) (\/) (A2 ^\ k)) . n) by Def2;

    end;

    theorem :: SETLIM_2:6

    

     Th6: ((A1 (\) A2) ^\ k) = ((A1 ^\ k) (\) (A2 ^\ k))

    proof

      let n be Element of NAT ;

      

      thus (((A1 (\) A2) ^\ k) . n) = ((A1 (\) A2) . (n + k)) by NAT_1:def 3

      .= ((A1 . (n + k)) \ (A2 . (n + k))) by Def3

      .= (((A1 ^\ k) . n) \ (A2 . (n + k))) by NAT_1:def 3

      .= (((A1 ^\ k) . n) \ ((A2 ^\ k) . n)) by NAT_1:def 3

      .= (((A1 ^\ k) (\) (A2 ^\ k)) . n) by Def3;

    end;

    theorem :: SETLIM_2:7

    

     Th7: ((A1 (\+\) A2) ^\ k) = ((A1 ^\ k) (\+\) (A2 ^\ k))

    proof

      let n be Element of NAT ;

      

      thus (((A1 (\+\) A2) ^\ k) . n) = ((A1 (\+\) A2) . (n + k)) by NAT_1:def 3

      .= ((A1 . (n + k)) \+\ (A2 . (n + k))) by Def4

      .= (((A1 ^\ k) . n) \+\ (A2 . (n + k))) by NAT_1:def 3

      .= (((A1 ^\ k) . n) \+\ ((A2 ^\ k) . n)) by NAT_1:def 3

      .= (((A1 ^\ k) (\+\) (A2 ^\ k)) . n) by Def4;

    end;

    theorem :: SETLIM_2:8

    

     Th8: ( Union (A1 (/\) A2)) c= (( Union A1) /\ ( Union A2))

    proof

      let x be object;

      assume x in ( Union (A1 (/\) A2));

      then

      consider n such that

       A1: x in ((A1 (/\) A2) . n) by PROB_1: 12;

      

       A2: x in ((A1 . n) /\ (A2 . n)) by A1, Def1;

      then x in (A2 . n) by XBOOLE_0:def 4;

      then

       A3: x in ( Union A2) by PROB_1: 12;

      x in (A1 . n) by A2, XBOOLE_0:def 4;

      then x in ( Union A1) by PROB_1: 12;

      hence thesis by A3, XBOOLE_0:def 4;

    end;

    theorem :: SETLIM_2:9

    

     Th9: ( Union (A1 (\/) A2)) = (( Union A1) \/ ( Union A2))

    proof

      thus ( Union (A1 (\/) A2)) c= (( Union A1) \/ ( Union A2))

      proof

        let x be object;

        assume x in ( Union (A1 (\/) A2));

        then

        consider n1 be Nat such that

         A1: x in ((A1 (\/) A2) . n1) by PROB_1: 12;

        

         A2: x in ((A1 . n1) \/ (A2 . n1)) by A1, Def2;

        per cases by A2, XBOOLE_0:def 3;

          suppose x in (A1 . n1);

          then x in ( Union A1) by PROB_1: 12;

          hence thesis by XBOOLE_0:def 3;

        end;

          suppose x in (A2 . n1);

          then x in ( Union A2) by PROB_1: 12;

          hence thesis by XBOOLE_0:def 3;

        end;

      end;

      let x be object;

      assume

       A3: x in (( Union A1) \/ ( Union A2));

      per cases by A3, XBOOLE_0:def 3;

        suppose x in ( Union A1);

        then

        consider n2 be Nat such that

         A4: x in (A1 . n2) by PROB_1: 12;

        x in ((A1 . n2) \/ (A2 . n2)) by A4, XBOOLE_0:def 3;

        then x in ((A1 (\/) A2) . n2) by Def2;

        hence thesis by PROB_1: 12;

      end;

        suppose x in ( Union A2);

        then

        consider n3 be Nat such that

         A5: x in (A2 . n3) by PROB_1: 12;

        x in ((A1 . n3) \/ (A2 . n3)) by A5, XBOOLE_0:def 3;

        then x in ((A1 (\/) A2) . n3) by Def2;

        hence thesis by PROB_1: 12;

      end;

    end;

    theorem :: SETLIM_2:10

    

     Th10: (( Union A1) \ ( Union A2)) c= ( Union (A1 (\) A2))

    proof

      let x be object;

      assume

       A1: x in (( Union A1) \ ( Union A2));

      then x in ( Union A1) by XBOOLE_0:def 5;

      then

      consider n1 be Nat such that

       A2: x in (A1 . n1) by PROB_1: 12;

       not x in ( Union A2) by A1, XBOOLE_0:def 5;

      then not x in (A2 . n1) by PROB_1: 12;

      then x in ((A1 . n1) \ (A2 . n1)) by A2, XBOOLE_0:def 5;

      then x in ((A1 (\) A2) . n1) by Def3;

      hence thesis by PROB_1: 12;

    end;

    theorem :: SETLIM_2:11

    

     Th11: (( Union A1) \+\ ( Union A2)) c= ( Union (A1 (\+\) A2))

    proof

      

       A1: (( Union A1) \ ( Union A2)) c= ( Union (A1 (\) A2)) & (( Union A2) \ ( Union A1)) c= ( Union (A2 (\) A1)) by Th10;

      (( Union (A1 (\) A2)) \/ ( Union (A2 (\) A1))) = ( Union ((A1 (\) A2) (\/) (A2 (\) A1))) by Th9

      .= ( Union (A1 (\+\) A2)) by Th3;

      hence thesis by A1, XBOOLE_1: 13;

    end;

    theorem :: SETLIM_2:12

    

     Th12: ( Intersection (A1 (/\) A2)) = (( Intersection A1) /\ ( Intersection A2))

    proof

      thus ( Intersection (A1 (/\) A2)) c= (( Intersection A1) /\ ( Intersection A2))

      proof

        let x be object;

        assume

         A1: x in ( Intersection (A1 (/\) A2));

        now

          let k;

          x in ((A1 (/\) A2) . k) by A1, PROB_1: 13;

          then x in ((A1 . k) /\ (A2 . k)) by Def1;

          hence x in (A1 . k) & x in (A2 . k) by XBOOLE_0:def 4;

        end;

        then x in ( Intersection A1) & x in ( Intersection A2) by PROB_1: 13;

        hence thesis by XBOOLE_0:def 4;

      end;

      let x be object;

      assume x in (( Intersection A1) /\ ( Intersection A2));

      then

       A2: x in ( Intersection A1) & x in ( Intersection A2) by XBOOLE_0:def 4;

      now

        let k;

        x in (A1 . k) & x in (A2 . k) by A2, PROB_1: 13;

        then x in ((A1 . k) /\ (A2 . k)) by XBOOLE_0:def 4;

        hence x in ((A1 (/\) A2) . k) by Def1;

      end;

      hence thesis by PROB_1: 13;

    end;

    theorem :: SETLIM_2:13

    

     Th13: (( Intersection A1) \/ ( Intersection A2)) c= ( Intersection (A1 (\/) A2))

    proof

      let x be object;

      assume

       A1: x in (( Intersection A1) \/ ( Intersection A2));

      per cases by A1, XBOOLE_0:def 3;

        suppose

         A2: x in ( Intersection A1);

        now

          let k;

          x in (A1 . k) by A2, PROB_1: 13;

          then x in ((A1 . k) \/ (A2 . k)) by XBOOLE_0:def 3;

          hence x in ((A1 (\/) A2) . k) by Def2;

        end;

        hence thesis by PROB_1: 13;

      end;

        suppose

         A3: x in ( Intersection A2);

        now

          let k;

          x in (A2 . k) by A3, PROB_1: 13;

          then x in ((A1 . k) \/ (A2 . k)) by XBOOLE_0:def 3;

          hence x in ((A1 (\/) A2) . k) by Def2;

        end;

        hence thesis by PROB_1: 13;

      end;

    end;

    theorem :: SETLIM_2:14

    

     Th14: ( Intersection (A1 (\) A2)) c= (( Intersection A1) \ ( Intersection A2))

    proof

      let x be object;

      assume

       A1: x in ( Intersection (A1 (\) A2));

       A2:

      now

        let k;

        x in ((A1 (\) A2) . k) by A1, PROB_1: 13;

        then x in ((A1 . k) \ (A2 . k)) by Def3;

        hence x in (A1 . k) & not x in (A2 . k) by XBOOLE_0:def 5;

      end;

      then not x in (A2 . 0 );

      then

       A3: not x in ( Intersection A2) by PROB_1: 13;

      x in ( Intersection A1) by A2, PROB_1: 13;

      hence thesis by A3, XBOOLE_0:def 5;

    end;

    definition

      let X;

      let A1 be SetSequence of X, A be Subset of X;

      :: SETLIM_2:def5

      func A (/\) A1 -> SetSequence of X means

      : Def5: for n holds (it . n) = (A /\ (A1 . n));

      existence

      proof

        deffunc F( Nat) = (A /\ (A1 . $1));

        consider f be SetSequence of X such that

         A1: for n be Element of NAT holds (f . n) = F(n) from FUNCT_2:sch 4;

        take f;

        let n;

        n in NAT by ORDINAL1:def 12;

        then (f . n) = F(n) by A1;

        hence thesis;

      end;

      uniqueness

      proof

        let A3 be SetSequence of X, A4 be SetSequence of X such that

         A2: for n holds (A3 . n) = (A /\ (A1 . n)) and

         A3: for n holds (A4 . n) = (A /\ (A1 . n));

        let n be Element of NAT ;

        

        thus (A3 . n) = (A /\ (A1 . n)) by A2

        .= (A4 . n) by A3;

      end;

      :: SETLIM_2:def6

      func A (\/) A1 -> SetSequence of X means

      : Def6: for n holds (it . n) = (A \/ (A1 . n));

      existence

      proof

        deffunc F( Nat) = (A \/ (A1 . $1));

        consider f be SetSequence of X such that

         A4: for n be Element of NAT holds (f . n) = F(n) from FUNCT_2:sch 4;

        take f;

        let n;

        n in NAT by ORDINAL1:def 12;

        then (f . n) = F(n) by A4;

        hence thesis;

      end;

      uniqueness

      proof

        let A3 be SetSequence of X, A4 be SetSequence of X such that

         A5: for n holds (A3 . n) = (A \/ (A1 . n)) and

         A6: for n holds (A4 . n) = (A \/ (A1 . n));

        let n be Element of NAT ;

        

        thus (A3 . n) = (A \/ (A1 . n)) by A5

        .= (A4 . n) by A6;

      end;

      :: SETLIM_2:def7

      func A (\) A1 -> SetSequence of X means

      : Def7: for n holds (it . n) = (A \ (A1 . n));

      existence

      proof

        deffunc F( Nat) = (A \ (A1 . $1));

        consider f be SetSequence of X such that

         A7: for n be Element of NAT holds (f . n) = F(n) from FUNCT_2:sch 4;

        take f;

        let n;

        n in NAT by ORDINAL1:def 12;

        then (f . n) = F(n) by A7;

        hence thesis;

      end;

      uniqueness

      proof

        let A3 be SetSequence of X, A4 be SetSequence of X such that

         A8: for n holds (A3 . n) = (A \ (A1 . n)) and

         A9: for n holds (A4 . n) = (A \ (A1 . n));

        let n be Element of NAT ;

        

        thus (A3 . n) = (A \ (A1 . n)) by A8

        .= (A4 . n) by A9;

      end;

      :: SETLIM_2:def8

      func A1 (\) A -> SetSequence of X means

      : Def8: for n holds (it . n) = ((A1 . n) \ A);

      existence

      proof

        deffunc F( Nat) = ((A1 . $1) \ A);

        consider f be SetSequence of X such that

         A10: for n be Element of NAT holds (f . n) = F(n) from FUNCT_2:sch 4;

        take f;

        let n;

        n in NAT by ORDINAL1:def 12;

        then (f . n) = F(n) by A10;

        hence thesis;

      end;

      uniqueness

      proof

        let A3 be SetSequence of X, A4 be SetSequence of X such that

         A11: for n holds (A3 . n) = ((A1 . n) \ A) and

         A12: for n holds (A4 . n) = ((A1 . n) \ A);

        let n be Element of NAT ;

        

        thus (A3 . n) = ((A1 . n) \ A) by A11

        .= (A4 . n) by A12;

      end;

      :: SETLIM_2:def9

      func A (\+\) A1 -> SetSequence of X means

      : Def9: for n holds (it . n) = (A \+\ (A1 . n));

      existence

      proof

        deffunc F( Nat) = (A \+\ (A1 . $1));

        consider f be SetSequence of X such that

         A13: for n be Element of NAT holds (f . n) = F(n) from FUNCT_2:sch 4;

        take f;

        let n;

        n in NAT by ORDINAL1:def 12;

        then (f . n) = F(n) by A13;

        hence thesis;

      end;

      uniqueness

      proof

        let A3 be SetSequence of X, A4 be SetSequence of X such that

         A14: for n holds (A3 . n) = (A \+\ (A1 . n)) and

         A15: for n holds (A4 . n) = (A \+\ (A1 . n));

        let n be Element of NAT ;

        

        thus (A3 . n) = (A \+\ (A1 . n)) by A14

        .= (A4 . n) by A15;

      end;

    end

    theorem :: SETLIM_2:15

    (A (\+\) A1) = ((A (\) A1) (\/) (A1 (\) A))

    proof

      let n be Element of NAT ;

      

      thus ((A (\+\) A1) . n) = (A \+\ (A1 . n)) by Def9

      .= (((A (\) A1) . n) \/ ((A1 . n) \ A)) by Def7

      .= (((A (\) A1) . n) \/ ((A1 (\) A) . n)) by Def8

      .= (((A (\) A1) (\/) (A1 (\) A)) . n) by Def2;

    end;

    theorem :: SETLIM_2:16

    

     Th16: ((A (/\) A1) ^\ k) = (A (/\) (A1 ^\ k))

    proof

      let n be Element of NAT ;

      

      thus (((A (/\) A1) ^\ k) . n) = ((A (/\) A1) . (n + k)) by NAT_1:def 3

      .= (A /\ (A1 . (n + k))) by Def5

      .= (A /\ ((A1 ^\ k) . n)) by NAT_1:def 3

      .= ((A (/\) (A1 ^\ k)) . n) by Def5;

    end;

    theorem :: SETLIM_2:17

    

     Th17: ((A (\/) A1) ^\ k) = (A (\/) (A1 ^\ k))

    proof

      let n be Element of NAT ;

      

      thus (((A (\/) A1) ^\ k) . n) = ((A (\/) A1) . (n + k)) by NAT_1:def 3

      .= (A \/ (A1 . (n + k))) by Def6

      .= (A \/ ((A1 ^\ k) . n)) by NAT_1:def 3

      .= ((A (\/) (A1 ^\ k)) . n) by Def6;

    end;

    theorem :: SETLIM_2:18

    

     Th18: ((A (\) A1) ^\ k) = (A (\) (A1 ^\ k))

    proof

      let n be Element of NAT ;

      

      thus (((A (\) A1) ^\ k) . n) = ((A (\) A1) . (n + k)) by NAT_1:def 3

      .= (A \ (A1 . (n + k))) by Def7

      .= (A \ ((A1 ^\ k) . n)) by NAT_1:def 3

      .= ((A (\) (A1 ^\ k)) . n) by Def7;

    end;

    theorem :: SETLIM_2:19

    

     Th19: ((A1 (\) A) ^\ k) = ((A1 ^\ k) (\) A)

    proof

      let n be Element of NAT ;

      

      thus (((A1 (\) A) ^\ k) . n) = ((A1 (\) A) . (n + k)) by NAT_1:def 3

      .= ((A1 . (n + k)) \ A) by Def8

      .= (((A1 ^\ k) . n) \ A) by NAT_1:def 3

      .= (((A1 ^\ k) (\) A) . n) by Def8;

    end;

    theorem :: SETLIM_2:20

    

     Th20: ((A (\+\) A1) ^\ k) = (A (\+\) (A1 ^\ k))

    proof

      let n be Element of NAT ;

      

      thus (((A (\+\) A1) ^\ k) . n) = ((A (\+\) A1) . (n + k)) by NAT_1:def 3

      .= (A \+\ (A1 . (n + k))) by Def9

      .= (A \+\ ((A1 ^\ k) . n)) by NAT_1:def 3

      .= ((A (\+\) (A1 ^\ k)) . n) by Def9;

    end;

    theorem :: SETLIM_2:21

    

     Th21: A1 is non-ascending implies (A (/\) A1) is non-ascending

    proof

      assume

       A1: A1 is non-ascending;

      for n, m st n <= m holds ((A (/\) A1) . m) c= ((A (/\) A1) . n)

      proof

        let n, m;

        assume n <= m;

        then (A1 . m) c= (A1 . n) by A1, PROB_1:def 4;

        then (A /\ (A1 . m)) c= (A /\ (A1 . n)) by XBOOLE_1: 27;

        then ((A (/\) A1) . m) c= (A /\ (A1 . n)) by Def5;

        hence thesis by Def5;

      end;

      hence thesis by PROB_1:def 4;

    end;

    theorem :: SETLIM_2:22

    

     Th22: A1 is non-descending implies (A (/\) A1) is non-descending

    proof

      assume

       A1: A1 is non-descending;

      for n, m st n <= m holds ((A (/\) A1) . n) c= ((A (/\) A1) . m)

      proof

        let n, m;

        assume n <= m;

        then (A1 . n) c= (A1 . m) by A1, PROB_1:def 5;

        then (A /\ (A1 . n)) c= (A /\ (A1 . m)) by XBOOLE_1: 27;

        then ((A (/\) A1) . n) c= (A /\ (A1 . m)) by Def5;

        hence thesis by Def5;

      end;

      hence thesis by PROB_1:def 5;

    end;

    theorem :: SETLIM_2:23

    A1 is monotone implies (A (/\) A1) is monotone

    proof

      assume

       A1: A1 is monotone;

      per cases by A1, SETLIM_1:def 1;

        suppose A1 is non-ascending;

        then (A (/\) A1) is non-ascending by Th21;

        hence thesis by SETLIM_1:def 1;

      end;

        suppose A1 is non-descending;

        then (A (/\) A1) is non-descending by Th22;

        hence thesis by SETLIM_1:def 1;

      end;

    end;

    theorem :: SETLIM_2:24

    

     Th24: A1 is non-ascending implies (A (\/) A1) is non-ascending

    proof

      assume

       A1: A1 is non-ascending;

      for n, m st n <= m holds ((A (\/) A1) . m) c= ((A (\/) A1) . n)

      proof

        let n, m;

        assume n <= m;

        then (A1 . m) c= (A1 . n) by A1, PROB_1:def 4;

        then (A \/ (A1 . m)) c= (A \/ (A1 . n)) by XBOOLE_1: 9;

        then ((A (\/) A1) . m) c= (A \/ (A1 . n)) by Def6;

        hence thesis by Def6;

      end;

      hence thesis by PROB_1:def 4;

    end;

    theorem :: SETLIM_2:25

    

     Th25: A1 is non-descending implies (A (\/) A1) is non-descending

    proof

      assume

       A1: A1 is non-descending;

      for n, m st n <= m holds ((A (\/) A1) . n) c= ((A (\/) A1) . m)

      proof

        let n, m;

        assume n <= m;

        then (A1 . n) c= (A1 . m) by A1, PROB_1:def 5;

        then (A \/ (A1 . n)) c= (A \/ (A1 . m)) by XBOOLE_1: 9;

        then ((A (\/) A1) . n) c= (A \/ (A1 . m)) by Def6;

        hence thesis by Def6;

      end;

      hence thesis by PROB_1:def 5;

    end;

    theorem :: SETLIM_2:26

    A1 is monotone implies (A (\/) A1) is monotone

    proof

      assume

       A1: A1 is monotone;

      per cases by A1, SETLIM_1:def 1;

        suppose A1 is non-ascending;

        then (A (\/) A1) is non-ascending by Th24;

        hence thesis by SETLIM_1:def 1;

      end;

        suppose A1 is non-descending;

        then (A (\/) A1) is non-descending by Th25;

        hence thesis by SETLIM_1:def 1;

      end;

    end;

    theorem :: SETLIM_2:27

    

     Th27: A1 is non-ascending implies (A (\) A1) is non-descending

    proof

      assume

       A1: A1 is non-ascending;

      for n, m st n <= m holds ((A (\) A1) . n) c= ((A (\) A1) . m)

      proof

        let n, m;

        assume n <= m;

        then (A1 . m) c= (A1 . n) by A1, PROB_1:def 4;

        then (A \ (A1 . n)) c= (A \ (A1 . m)) by XBOOLE_1: 34;

        then ((A (\) A1) . n) c= (A \ (A1 . m)) by Def7;

        hence thesis by Def7;

      end;

      hence thesis by PROB_1:def 5;

    end;

    theorem :: SETLIM_2:28

    

     Th28: A1 is non-descending implies (A (\) A1) is non-ascending

    proof

      assume

       A1: A1 is non-descending;

      for n, m st n <= m holds ((A (\) A1) . m) c= ((A (\) A1) . n)

      proof

        let n, m;

        assume n <= m;

        then (A1 . n) c= (A1 . m) by A1, PROB_1:def 5;

        then (A \ (A1 . m)) c= (A \ (A1 . n)) by XBOOLE_1: 34;

        then ((A (\) A1) . m) c= (A \ (A1 . n)) by Def7;

        hence thesis by Def7;

      end;

      hence thesis by PROB_1:def 4;

    end;

    theorem :: SETLIM_2:29

    A1 is monotone implies (A (\) A1) is monotone

    proof

      assume

       A1: A1 is monotone;

      per cases by A1, SETLIM_1:def 1;

        suppose A1 is non-ascending;

        then (A (\) A1) is non-descending by Th27;

        hence thesis by SETLIM_1:def 1;

      end;

        suppose A1 is non-descending;

        then (A (\) A1) is non-ascending by Th28;

        hence thesis by SETLIM_1:def 1;

      end;

    end;

    theorem :: SETLIM_2:30

    

     Th30: A1 is non-ascending implies (A1 (\) A) is non-ascending

    proof

      assume

       A1: A1 is non-ascending;

      for n, m st n <= m holds ((A1 (\) A) . m) c= ((A1 (\) A) . n)

      proof

        let n, m;

        assume n <= m;

        then (A1 . m) c= (A1 . n) by A1, PROB_1:def 4;

        then ((A1 . m) \ A) c= ((A1 . n) \ A) by XBOOLE_1: 33;

        then ((A1 (\) A) . m) c= ((A1 . n) \ A) by Def8;

        hence thesis by Def8;

      end;

      hence thesis by PROB_1:def 4;

    end;

    theorem :: SETLIM_2:31

    

     Th31: A1 is non-descending implies (A1 (\) A) is non-descending

    proof

      assume

       A1: A1 is non-descending;

      for n, m st n <= m holds ((A1 (\) A) . n) c= ((A1 (\) A) . m)

      proof

        let n, m;

        assume n <= m;

        then (A1 . n) c= (A1 . m) by A1, PROB_1:def 5;

        then ((A1 . n) \ A) c= ((A1 . m) \ A) by XBOOLE_1: 33;

        then ((A1 (\) A) . n) c= ((A1 . m) \ A) by Def8;

        hence thesis by Def8;

      end;

      hence thesis by PROB_1:def 5;

    end;

    theorem :: SETLIM_2:32

    A1 is monotone implies (A1 (\) A) is monotone

    proof

      assume

       A1: A1 is monotone;

      per cases by A1, SETLIM_1:def 1;

        suppose A1 is non-ascending;

        then (A1 (\) A) is non-ascending by Th30;

        hence thesis by SETLIM_1:def 1;

      end;

        suppose A1 is non-descending;

        then (A1 (\) A) is non-descending by Th31;

        hence thesis by SETLIM_1:def 1;

      end;

    end;

    theorem :: SETLIM_2:33

    

     Th33: ( Intersection (A (/\) A1)) = (A /\ ( Intersection A1))

    proof

      thus ( Intersection (A (/\) A1)) c= (A /\ ( Intersection A1))

      proof

        let x be object;

        assume

         A1: x in ( Intersection (A (/\) A1));

         A2:

        now

          let k;

          x in ((A (/\) A1) . k) by A1, PROB_1: 13;

          then x in (A /\ (A1 . k)) by Def5;

          hence x in A & x in (A1 . k) by XBOOLE_0:def 4;

        end;

        then x in ( Intersection A1) by PROB_1: 13;

        hence thesis by A2, XBOOLE_0:def 4;

      end;

      let x be object;

      assume

       A3: x in (A /\ ( Intersection A1));

      then

       A4: x in ( Intersection A1) by XBOOLE_0:def 4;

      now

        let k;

        x in A & x in (A1 . k) by A3, A4, PROB_1: 13, XBOOLE_0:def 4;

        then x in (A /\ (A1 . k)) by XBOOLE_0:def 4;

        hence x in ((A (/\) A1) . k) by Def5;

      end;

      hence thesis by PROB_1: 13;

    end;

    theorem :: SETLIM_2:34

    

     Th34: ( Intersection (A (\/) A1)) = (A \/ ( Intersection A1))

    proof

      thus ( Intersection (A (\/) A1)) c= (A \/ ( Intersection A1))

      proof

        let x be object;

        assume

         A1: x in ( Intersection (A (\/) A1));

         A2:

        now

          let k;

          x in ((A (\/) A1) . k) by A1, PROB_1: 13;

          then x in (A \/ (A1 . k)) by Def6;

          hence x in A or x in (A1 . k) by XBOOLE_0:def 3;

        end;

        per cases by A2;

          suppose x in A;

          hence thesis by XBOOLE_0:def 3;

        end;

          suppose x in (A1 . k);

          then x in ( Intersection A1) by PROB_1: 13;

          hence thesis by XBOOLE_0:def 3;

        end;

      end;

      let x be object;

      assume

       A3: x in (A \/ ( Intersection A1));

      per cases by A3, XBOOLE_0:def 3;

        suppose

         A4: x in A;

        now

          let k;

          x in (A \/ (A1 . k)) by A4, XBOOLE_0:def 3;

          hence x in ((A (\/) A1) . k) by Def6;

        end;

        hence thesis by PROB_1: 13;

      end;

        suppose

         A5: x in ( Intersection A1);

        now

          let k;

          x in (A1 . k) by A5, PROB_1: 13;

          then x in (A \/ (A1 . k)) by XBOOLE_0:def 3;

          hence x in ((A (\/) A1) . k) by Def6;

        end;

        hence thesis by PROB_1: 13;

      end;

    end;

    theorem :: SETLIM_2:35

    

     Th35: ( Intersection (A (\) A1)) c= (A \ ( Intersection A1))

    proof

      let x be object;

      assume

       A1: x in ( Intersection (A (\) A1));

       A2:

      now

        let k;

        x in ((A (\) A1) . k) by A1, PROB_1: 13;

        then x in (A \ (A1 . k)) by Def7;

        hence x in A & not x in (A1 . k) by XBOOLE_0:def 5;

      end;

      then not x in (A1 . 0 );

      then not x in ( Intersection A1) by PROB_1: 13;

      hence thesis by A2, XBOOLE_0:def 5;

    end;

    theorem :: SETLIM_2:36

    

     Th36: ( Intersection (A1 (\) A)) = (( Intersection A1) \ A)

    proof

      thus ( Intersection (A1 (\) A)) c= (( Intersection A1) \ A)

      proof

        let x be object;

        assume

         A1: x in ( Intersection (A1 (\) A));

         A2:

        now

          let k;

          x in ((A1 (\) A) . k) by A1, PROB_1: 13;

          then x in ((A1 . k) \ A) by Def8;

          hence x in (A1 . k) & not x in A by XBOOLE_0:def 5;

        end;

        then x in ( Intersection A1) by PROB_1: 13;

        hence thesis by A2, XBOOLE_0:def 5;

      end;

      let x be object;

      assume

       A3: x in (( Intersection A1) \ A);

      then

       A4: x in ( Intersection A1) by XBOOLE_0:def 5;

      now

        let k;

        x in (A1 . k) & not x in A by A3, A4, PROB_1: 13, XBOOLE_0:def 5;

        then x in ((A1 . k) \ A) by XBOOLE_0:def 5;

        hence x in ((A1 (\) A) . k) by Def8;

      end;

      hence thesis by PROB_1: 13;

    end;

    theorem :: SETLIM_2:37

    

     Th37: ( Intersection (A (\+\) A1)) c= (A \+\ ( Intersection A1))

    proof

      let x be object;

      assume

       A1: x in ( Intersection (A (\+\) A1));

       A2:

      now

        let n;

        x in ((A (\+\) A1) . n) by A1, PROB_1: 13;

        then x in (A \+\ (A1 . n)) by Def9;

        hence x in A & not x in (A1 . n) or not x in A & x in (A1 . n) by XBOOLE_0: 1;

      end;

      assume not x in (A \+\ ( Intersection A1));

      then

       A3: not x in A & not x in ( Intersection A1) or x in ( Intersection A1) & x in A by XBOOLE_0: 1;

      per cases by A3, PROB_1: 13;

        suppose not x in A & not for n holds x in (A1 . n);

        hence contradiction by A2;

      end;

        suppose

         A4: x in A & for n holds x in (A1 . n);

        then x in (A1 . 0 );

        hence contradiction by A2, A4;

      end;

    end;

    theorem :: SETLIM_2:38

    

     Th38: ( Union (A (/\) A1)) = (A /\ ( Union A1))

    proof

      thus ( Union (A (/\) A1)) c= (A /\ ( Union A1))

      proof

        let x be object;

        assume x in ( Union (A (/\) A1));

        then

        consider n such that

         A1: x in ((A (/\) A1) . n) by PROB_1: 12;

        

         A2: x in (A /\ (A1 . n)) by A1, Def5;

        then x in (A1 . n) by XBOOLE_0:def 4;

        then

         A3: x in ( Union A1) by PROB_1: 12;

        x in A by A2, XBOOLE_0:def 4;

        hence thesis by A3, XBOOLE_0:def 4;

      end;

      let x be object;

      assume

       A4: x in (A /\ ( Union A1));

      then x in ( Union A1) by XBOOLE_0:def 4;

      then

      consider n such that

       A5: x in (A1 . n) by PROB_1: 12;

      x in A by A4, XBOOLE_0:def 4;

      then x in (A /\ (A1 . n)) by A5, XBOOLE_0:def 4;

      then x in ((A (/\) A1) . n) by Def5;

      hence thesis by PROB_1: 12;

    end;

    theorem :: SETLIM_2:39

    

     Th39: ( Union (A (\/) A1)) = (A \/ ( Union A1))

    proof

      thus ( Union (A (\/) A1)) c= (A \/ ( Union A1))

      proof

        let x be object;

        assume

         A1: x in ( Union (A (\/) A1));

        

         A2: x in A or ex k st x in (A1 . k)

        proof

          consider k such that

           A3: x in ((A (\/) A1) . k) by A1, PROB_1: 12;

          x in (A \/ (A1 . k)) by A3, Def6;

          then x in A or x in (A1 . k) by XBOOLE_0:def 3;

          hence thesis;

        end;

        per cases by A2;

          suppose x in A;

          hence thesis by XBOOLE_0:def 3;

        end;

          suppose ex k st x in (A1 . k);

          then x in ( Union A1) by PROB_1: 12;

          hence thesis by XBOOLE_0:def 3;

        end;

      end;

      let x be object;

      assume

       A4: x in (A \/ ( Union A1));

      per cases by A4, XBOOLE_0:def 3;

        suppose x in A;

        then x in (A \/ (A1 . 1)) by XBOOLE_0:def 3;

        then x in ((A (\/) A1) . 1) by Def6;

        hence thesis by PROB_1: 12;

      end;

        suppose x in ( Union A1);

        then

        consider k such that

         A5: x in (A1 . k) by PROB_1: 12;

        x in (A \/ (A1 . k)) by A5, XBOOLE_0:def 3;

        then x in ((A (\/) A1) . k) by Def6;

        hence thesis by PROB_1: 12;

      end;

    end;

    theorem :: SETLIM_2:40

    

     Th40: (A \ ( Union A1)) c= ( Union (A (\) A1))

    proof

      let x be object;

      assume

       A1: x in (A \ ( Union A1));

      then

       A2: not x in ( Union A1) by XBOOLE_0:def 5;

      now

        let k;

        x in A & not x in (A1 . k) by A1, A2, PROB_1: 12, XBOOLE_0:def 5;

        then x in (A \ (A1 . k)) by XBOOLE_0:def 5;

        hence x in ((A (\) A1) . k) by Def7;

      end;

      then x in ((A (\) A1) . 1);

      hence thesis by PROB_1: 12;

    end;

    theorem :: SETLIM_2:41

    

     Th41: ( Union (A1 (\) A)) = (( Union A1) \ A)

    proof

      thus ( Union (A1 (\) A)) c= (( Union A1) \ A)

      proof

        let x be object;

        assume

         A1: x in ( Union (A1 (\) A));

        

         A2: ex k st x in (A1 . k) & not x in A

        proof

          consider k such that

           A3: x in ((A1 (\) A) . k) by A1, PROB_1: 12;

          x in ((A1 . k) \ A) by A3, Def8;

          then x in (A1 . k) & not x in A by XBOOLE_0:def 5;

          hence thesis;

        end;

        then x in ( Union A1) by PROB_1: 12;

        hence thesis by A2, XBOOLE_0:def 5;

      end;

      let x be object;

      assume

       A4: x in (( Union A1) \ A);

      then

       A5: not x in A by XBOOLE_0:def 5;

      

       A6: x in ( Union A1) by A4, XBOOLE_0:def 5;

      ex k st x in ((A1 (\) A) . k)

      proof

        consider k such that

         A7: x in (A1 . k) by A6, PROB_1: 12;

        x in ((A1 . k) \ A) by A5, A7, XBOOLE_0:def 5;

        then x in ((A1 (\) A) . k) by Def8;

        hence thesis;

      end;

      hence thesis by PROB_1: 12;

    end;

    theorem :: SETLIM_2:42

    

     Th42: (A \+\ ( Union A1)) c= ( Union (A (\+\) A1))

    proof

      let x be object;

      assume

       A1: x in (A \+\ ( Union A1));

      per cases by A1, XBOOLE_0: 1;

        suppose

         A2: x in A & not x in ( Union A1);

        then not x in (A1 . 0 ) by PROB_1: 12;

        then x in (A \+\ (A1 . 0 )) by A2, XBOOLE_0: 1;

        then x in ((A (\+\) A1) . 0 ) by Def9;

        hence thesis by PROB_1: 12;

      end;

        suppose

         A3: not x in A & x in ( Union A1);

        then

        consider n1 be Nat such that

         A4: x in (A1 . n1) by PROB_1: 12;

        x in (A \+\ (A1 . n1)) by A3, A4, XBOOLE_0: 1;

        then x in ((A (\+\) A1) . n1) by Def9;

        hence thesis by PROB_1: 12;

      end;

    end;

    theorem :: SETLIM_2:43

    (( inferior_setsequence (A1 (/\) A2)) . n) = ((( inferior_setsequence A1) . n) /\ (( inferior_setsequence A2) . n))

    proof

      (( inferior_setsequence (A1 (/\) A2)) . n) = ( Intersection ((A1 (/\) A2) ^\ n)) by Th1

      .= ( Intersection ((A1 ^\ n) (/\) (A2 ^\ n))) by Th4

      .= (( Intersection (A1 ^\ n)) /\ ( Intersection (A2 ^\ n))) by Th12

      .= ((( inferior_setsequence A1) . n) /\ ( Intersection (A2 ^\ n))) by Th1

      .= ((( inferior_setsequence A1) . n) /\ (( inferior_setsequence A2) . n)) by Th1;

      hence thesis;

    end;

    theorem :: SETLIM_2:44

    ((( inferior_setsequence A1) . n) \/ (( inferior_setsequence A2) . n)) c= (( inferior_setsequence (A1 (\/) A2)) . n)

    proof

      

       A1: ( Intersection ((A1 ^\ n) (\/) (A2 ^\ n))) = ( Intersection ((A1 (\/) A2) ^\ n)) by Th5

      .= (( inferior_setsequence (A1 (\/) A2)) . n) by Th1;

      ((( inferior_setsequence A1) . n) \/ (( inferior_setsequence A2) . n)) = (( Intersection (A1 ^\ n)) \/ (( inferior_setsequence A2) . n)) by Th1

      .= (( Intersection (A1 ^\ n)) \/ ( Intersection (A2 ^\ n))) by Th1;

      hence thesis by A1, Th13;

    end;

    theorem :: SETLIM_2:45

    (( inferior_setsequence (A1 (\) A2)) . n) c= ((( inferior_setsequence A1) . n) \ (( inferior_setsequence A2) . n))

    proof

      (( inferior_setsequence (A1 (\) A2)) . n) = ( Intersection ((A1 (\) A2) ^\ n)) by Th1

      .= ( Intersection ((A1 ^\ n) (\) (A2 ^\ n))) by Th6;

      then (( inferior_setsequence (A1 (\) A2)) . n) c= (( Intersection (A1 ^\ n)) \ ( Intersection (A2 ^\ n))) by Th14;

      then (( inferior_setsequence (A1 (\) A2)) . n) c= ((( inferior_setsequence A1) . n) \ ( Intersection (A2 ^\ n))) by Th1;

      hence thesis by Th1;

    end;

    theorem :: SETLIM_2:46

    (( superior_setsequence (A1 (/\) A2)) . n) c= ((( superior_setsequence A1) . n) /\ (( superior_setsequence A2) . n))

    proof

      (( superior_setsequence (A1 (/\) A2)) . n) = ( Union ((A1 (/\) A2) ^\ n)) by Th2

      .= ( Union ((A1 ^\ n) (/\) (A2 ^\ n))) by Th4;

      then (( superior_setsequence (A1 (/\) A2)) . n) c= (( Union (A1 ^\ n)) /\ ( Union (A2 ^\ n))) by Th8;

      then (( superior_setsequence (A1 (/\) A2)) . n) c= ((( superior_setsequence A1) . n) /\ ( Union (A2 ^\ n))) by Th2;

      hence thesis by Th2;

    end;

    theorem :: SETLIM_2:47

    (( superior_setsequence (A1 (\/) A2)) . n) = ((( superior_setsequence A1) . n) \/ (( superior_setsequence A2) . n))

    proof

      (( superior_setsequence (A1 (\/) A2)) . n) = ( Union ((A1 (\/) A2) ^\ n)) by Th2

      .= ( Union ((A1 ^\ n) (\/) (A2 ^\ n))) by Th5

      .= (( Union (A1 ^\ n)) \/ ( Union (A2 ^\ n))) by Th9

      .= ((( superior_setsequence A1) . n) \/ ( Union (A2 ^\ n))) by Th2;

      hence thesis by Th2;

    end;

    theorem :: SETLIM_2:48

    ((( superior_setsequence A1) . n) \ (( superior_setsequence A2) . n)) c= (( superior_setsequence (A1 (\) A2)) . n)

    proof

      ((( superior_setsequence A1) . n) \ (( superior_setsequence A2) . n)) = (( Union (A1 ^\ n)) \ (( superior_setsequence A2) . n)) by Th2

      .= (( Union (A1 ^\ n)) \ ( Union (A2 ^\ n))) by Th2;

      then ((( superior_setsequence A1) . n) \ (( superior_setsequence A2) . n)) c= ( Union ((A1 ^\ n) (\) (A2 ^\ n))) by Th10;

      then ((( superior_setsequence A1) . n) \ (( superior_setsequence A2) . n)) c= ( Union ((A1 (\) A2) ^\ n)) by Th6;

      hence thesis by Th2;

    end;

    theorem :: SETLIM_2:49

    ((( superior_setsequence A1) . n) \+\ (( superior_setsequence A2) . n)) c= (( superior_setsequence (A1 (\+\) A2)) . n)

    proof

      ((( superior_setsequence A1) . n) \+\ (( superior_setsequence A2) . n)) = (( Union (A1 ^\ n)) \+\ (( superior_setsequence A2) . n)) by Th2

      .= (( Union (A1 ^\ n)) \+\ ( Union (A2 ^\ n))) by Th2;

      then ((( superior_setsequence A1) . n) \+\ (( superior_setsequence A2) . n)) c= ( Union ((A1 ^\ n) (\+\) (A2 ^\ n))) by Th11;

      then ((( superior_setsequence A1) . n) \+\ (( superior_setsequence A2) . n)) c= ( Union ((A1 (\+\) A2) ^\ n)) by Th7;

      hence thesis by Th2;

    end;

    theorem :: SETLIM_2:50

    

     Th50: (( inferior_setsequence (A (/\) A1)) . n) = (A /\ (( inferior_setsequence A1) . n))

    proof

      (( inferior_setsequence (A (/\) A1)) . n) = ( Intersection ((A (/\) A1) ^\ n)) by Th1

      .= ( Intersection (A (/\) (A1 ^\ n))) by Th16

      .= (A /\ ( Intersection (A1 ^\ n))) by Th33

      .= (A /\ (( inferior_setsequence A1) . n)) by Th1;

      hence thesis;

    end;

    theorem :: SETLIM_2:51

    

     Th51: (( inferior_setsequence (A (\/) A1)) . n) = (A \/ (( inferior_setsequence A1) . n))

    proof

      (( inferior_setsequence (A (\/) A1)) . n) = ( Intersection ((A (\/) A1) ^\ n)) by Th1

      .= ( Intersection (A (\/) (A1 ^\ n))) by Th17

      .= (A \/ ( Intersection (A1 ^\ n))) by Th34

      .= (A \/ (( inferior_setsequence A1) . n)) by Th1;

      hence thesis;

    end;

    theorem :: SETLIM_2:52

    (( inferior_setsequence (A (\) A1)) . n) c= (A \ (( inferior_setsequence A1) . n))

    proof

      (( inferior_setsequence (A (\) A1)) . n) = ( Intersection ((A (\) A1) ^\ n)) by Th1

      .= ( Intersection (A (\) (A1 ^\ n))) by Th18;

      then (( inferior_setsequence (A (\) A1)) . n) c= (A \ ( Intersection (A1 ^\ n))) by Th35;

      hence thesis by Th1;

    end;

    theorem :: SETLIM_2:53

    

     Th53: (( inferior_setsequence (A1 (\) A)) . n) = ((( inferior_setsequence A1) . n) \ A)

    proof

      (( inferior_setsequence (A1 (\) A)) . n) = ( Intersection ((A1 (\) A) ^\ n)) by Th1

      .= ( Intersection ((A1 ^\ n) (\) A)) by Th19

      .= (( Intersection (A1 ^\ n)) \ A) by Th36

      .= ((( inferior_setsequence A1) . n) \ A) by Th1;

      hence thesis;

    end;

    theorem :: SETLIM_2:54

    (( inferior_setsequence (A (\+\) A1)) . n) c= (A \+\ (( inferior_setsequence A1) . n))

    proof

      (( inferior_setsequence (A (\+\) A1)) . n) = ( Intersection ((A (\+\) A1) ^\ n)) by Th1

      .= ( Intersection (A (\+\) (A1 ^\ n))) by Th20;

      then (( inferior_setsequence (A (\+\) A1)) . n) c= (A \+\ ( Intersection (A1 ^\ n))) by Th37;

      hence thesis by Th1;

    end;

    theorem :: SETLIM_2:55

    

     Th55: (( superior_setsequence (A (/\) A1)) . n) = (A /\ (( superior_setsequence A1) . n))

    proof

      (( superior_setsequence (A (/\) A1)) . n) = ( Union ((A (/\) A1) ^\ n)) by Th2

      .= ( Union (A (/\) (A1 ^\ n))) by Th16

      .= (A /\ ( Union (A1 ^\ n))) by Th38

      .= (A /\ (( superior_setsequence A1) . n)) by Th2;

      hence thesis;

    end;

    theorem :: SETLIM_2:56

    

     Th56: (( superior_setsequence (A (\/) A1)) . n) = (A \/ (( superior_setsequence A1) . n))

    proof

      (( superior_setsequence (A (\/) A1)) . n) = ( Union ((A (\/) A1) ^\ n)) by Th2

      .= ( Union (A (\/) (A1 ^\ n))) by Th17

      .= (A \/ ( Union (A1 ^\ n))) by Th39

      .= (A \/ (( superior_setsequence A1) . n)) by Th2;

      hence thesis;

    end;

    theorem :: SETLIM_2:57

    (A \ (( superior_setsequence A1) . n)) c= (( superior_setsequence (A (\) A1)) . n)

    proof

      (A \ (( superior_setsequence A1) . n)) = (A \ ( Union (A1 ^\ n))) by Th2;

      then (A \ (( superior_setsequence A1) . n)) c= ( Union (A (\) (A1 ^\ n))) by Th40;

      then (A \ (( superior_setsequence A1) . n)) c= ( Union ((A (\) A1) ^\ n)) by Th18;

      hence thesis by Th2;

    end;

    theorem :: SETLIM_2:58

    

     Th58: (( superior_setsequence (A1 (\) A)) . n) = ((( superior_setsequence A1) . n) \ A)

    proof

      reconsider X1 = ( superior_setsequence A1) as SetSequence of X;

      reconsider X2 = ( superior_setsequence (A1 (\) A)) as SetSequence of X;

      

       A1: ((X1 . n) \ A) c= (X2 . n)

      proof

        let x be object;

        assume

         A2: x in ((X1 . n) \ A);

        then

         A3: not x in A by XBOOLE_0:def 5;

        

         A4: x in (X1 . n) by A2, XBOOLE_0:def 5;

        ex k st x in ((A1 (\) A) . (n + k))

        proof

          consider k such that

           A5: x in (A1 . (n + k)) by A4, SETLIM_1: 20;

          x in ((A1 . (n + k)) \ A) by A3, A5, XBOOLE_0:def 5;

          then x in ((A1 (\) A) . (n + k)) by Def8;

          hence thesis;

        end;

        hence thesis by SETLIM_1: 20;

      end;

      (X2 . n) c= ((X1 . n) \ A)

      proof

        let x be object;

        assume

         A6: x in (X2 . n);

        

         A7: ex k st x in (A1 . (n + k)) & not x in A

        proof

          consider k such that

           A8: x in ((A1 (\) A) . (n + k)) by A6, SETLIM_1: 20;

          x in ((A1 . (n + k)) \ A) by A8, Def8;

          then x in (A1 . (n + k)) & not x in A by XBOOLE_0:def 5;

          hence thesis;

        end;

        then x in (X1 . n) by SETLIM_1: 20;

        hence thesis by A7, XBOOLE_0:def 5;

      end;

      hence thesis by A1;

    end;

    theorem :: SETLIM_2:59

    (A \+\ (( superior_setsequence A1) . n)) c= (( superior_setsequence (A (\+\) A1)) . n)

    proof

      (A \+\ (( superior_setsequence A1) . n)) = (A \+\ ( Union (A1 ^\ n))) by Th2;

      then (A \+\ (( superior_setsequence A1) . n)) c= ( Union (A (\+\) (A1 ^\ n))) by Th42;

      then (A \+\ (( superior_setsequence A1) . n)) c= ( Union ((A (\+\) A1) ^\ n)) by Th20;

      hence thesis by Th2;

    end;

    theorem :: SETLIM_2:60

    

     Th60: ( lim_inf (A1 (/\) A2)) = (( lim_inf A1) /\ ( lim_inf A2))

    proof

      ((A1 (/\) A2) . n) = ((A1 . n) /\ (A2 . n)) by Def1;

      hence thesis by KURATO_0: 10;

    end;

    theorem :: SETLIM_2:61

    

     Th61: (( lim_inf A1) \/ ( lim_inf A2)) c= ( lim_inf (A1 (\/) A2))

    proof

      ((A1 (\/) A2) . n) = ((A1 . n) \/ (A2 . n)) by Def2;

      hence thesis by KURATO_0: 12;

    end;

    theorem :: SETLIM_2:62

    

     Th62: ( lim_inf (A1 (\) A2)) c= (( lim_inf A1) \ ( lim_inf A2))

    proof

      let x be object;

      assume x in ( lim_inf (A1 (\) A2));

      then

      consider n such that

       A1: for k holds x in ((A1 (\) A2) . (n + k)) by KURATO_0: 4;

       A2:

      now

        let k;

        x in ((A1 (\) A2) . (n + k)) by A1;

        then x in ((A1 . (n + k)) \ (A2 . (n + k))) by Def3;

        hence x in (A1 . (n + k)) & not x in (A2 . (n + k)) by XBOOLE_0:def 5;

      end;

      

       A3: not x in ( lim_inf A2)

      proof

        assume x in ( lim_inf A2);

        then

        consider n1 be Nat such that

         A4: for k holds x in (A2 . (n1 + k)) by KURATO_0: 4;

        x in (A2 . (n1 + n)) by A4;

        hence contradiction by A2;

      end;

      x in ( lim_inf A1) by A2, KURATO_0: 4;

      hence thesis by A3, XBOOLE_0:def 5;

    end;

    theorem :: SETLIM_2:63

    

     Th63: A1 is convergent or A2 is convergent implies ( lim_inf (A1 (\/) A2)) = (( lim_inf A1) \/ ( lim_inf A2))

    proof

      

       A1: for A1, A2 st A1 is convergent holds ( lim_inf (A1 (\/) A2)) = (( lim_inf A1) \/ ( lim_inf A2))

      proof

        let A1, A2;

        assume

         A2: A1 is convergent;

        thus ( lim_inf (A1 (\/) A2)) c= (( lim_inf A1) \/ ( lim_inf A2))

        proof

          let x be object;

          assume x in ( lim_inf (A1 (\/) A2));

          then

          consider n1 be Nat such that

           A3: for k holds x in ((A1 (\/) A2) . (n1 + k)) by KURATO_0: 4;

           A4:

          now

            let n;

            x in ((A1 (\/) A2) . (n1 + n)) by A3;

            then x in ((A1 . (n1 + n)) \/ (A2 . (n1 + n))) by Def2;

            hence x in (A1 . (n1 + n)) or x in (A2 . (n1 + n)) by XBOOLE_0:def 3;

          end;

          x in (( lim_inf A1) \/ ( lim_inf A2))

          proof

            assume

             A5: not x in (( lim_inf A1) \/ ( lim_inf A2));

            then not x in ( lim_inf A1) by XBOOLE_0:def 3;

            then not x in ( lim_sup A1) by A2, KURATO_0:def 5;

            then

            consider n2 be Nat such that

             A6: for k holds not x in (A1 . (n2 + k)) by KURATO_0: 5;

             not x in ( lim_inf A2) by A5, XBOOLE_0:def 3;

            then

            consider k1 be Nat such that

             A7: not x in (A2 . ((n1 + n2) + k1)) by KURATO_0: 4;

             not x in (A1 . (n2 + (n1 + k1))) by A6;

            then not x in (A1 . (n1 + (n2 + k1)));

            hence contradiction by A4, A7;

          end;

          hence thesis;

        end;

        thus thesis by Th61;

      end;

      assume

       A8: A1 is convergent or A2 is convergent;

      per cases by A8;

        suppose A1 is convergent;

        hence thesis by A1;

      end;

        suppose A2 is convergent;

        hence thesis by A1;

      end;

    end;

    theorem :: SETLIM_2:64

    

     Th64: A2 is convergent implies ( lim_inf (A1 (\) A2)) = (( lim_inf A1) \ ( lim_inf A2))

    proof

      assume

       A1: A2 is convergent;

      thus ( lim_inf (A1 (\) A2)) c= (( lim_inf A1) \ ( lim_inf A2)) by Th62;

      thus (( lim_inf A1) \ ( lim_inf A2)) c= ( lim_inf (A1 (\) A2))

      proof

        let x be object;

        assume

         A2: x in (( lim_inf A1) \ ( lim_inf A2));

        then x in ( lim_inf A1) by XBOOLE_0:def 5;

        then

        consider n0 be Nat such that

         A3: for k holds x in (A1 . (n0 + k)) by KURATO_0: 4;

         not x in ( lim_inf A2) by A2, XBOOLE_0:def 5;

        then not x in ( lim_sup A2) by A1, KURATO_0:def 5;

        then

        consider n1 be Nat such that

         A4: for k holds not x in (A2 . (n1 + k)) by KURATO_0: 5;

        now

          let k;

          x in (A1 . (n0 + (n1 + k))) & not x in (A2 . (n1 + (n0 + k))) by A3, A4;

          then x in ((A1 . ((n0 + n1) + k)) \ (A2 . ((n0 + n1) + k))) by XBOOLE_0:def 5;

          hence x in ((A1 (\) A2) . ((n0 + n1) + k)) by Def3;

        end;

        hence thesis by KURATO_0: 4;

      end;

    end;

    theorem :: SETLIM_2:65

    

     Th65: A1 is convergent or A2 is convergent implies ( lim_inf (A1 (\+\) A2)) c= (( lim_inf A1) \+\ ( lim_inf A2))

    proof

      

       A1: for A1, A2 st A1 is convergent holds ( lim_inf (A1 (\+\) A2)) c= (( lim_inf A1) \+\ ( lim_inf A2))

      proof

        let A1, A2;

        assume

         A2: A1 is convergent;

        thus ( lim_inf (A1 (\+\) A2)) c= (( lim_inf A1) \+\ ( lim_inf A2))

        proof

          let x be object;

          assume x in ( lim_inf (A1 (\+\) A2));

          then

          consider n1 be Nat such that

           A3: for k holds x in ((A1 (\+\) A2) . (n1 + k)) by KURATO_0: 4;

           A4:

          now

            let k;

            x in ((A1 (\+\) A2) . (n1 + k)) by A3;

            then x in ((A1 . (n1 + k)) \+\ (A2 . (n1 + k))) by Def4;

            hence x in (A1 . (n1 + k)) & not x in (A2 . (n1 + k)) or not x in (A1 . (n1 + k)) & x in (A2 . (n1 + k)) by XBOOLE_0: 1;

          end;

          assume

           A5: not x in (( lim_inf A1) \+\ ( lim_inf A2));

          per cases by A5, XBOOLE_0: 1;

            suppose

             A6: not x in ( lim_inf A1) & not x in ( lim_inf A2);

            then not x in ( lim_sup A1) by A2, KURATO_0:def 5;

            then

            consider n2 be Nat such that

             A7: for k holds not x in (A1 . (n2 + k)) by KURATO_0: 5;

            consider k1 be Nat such that

             A8: not x in (A2 . ((n1 + n2) + k1)) by A6, KURATO_0: 4;

            

             A9: x in (A1 . (n1 + (n2 + k1))) & not x in (A2 . (n1 + (n2 + k1))) or not x in (A1 . (n1 + (n2 + k1))) & x in (A2 . (n1 + (n2 + k1))) by A4;

             not x in (A1 . (n2 + (n1 + k1))) by A7;

            hence contradiction by A8, A9;

          end;

            suppose

             A10: x in ( lim_inf A1) & x in ( lim_inf A2);

            then

            consider n3 be Nat such that

             A11: for k holds x in (A2 . (n3 + k)) by KURATO_0: 4;

            consider n2 be Nat such that

             A12: for k holds x in (A1 . (n2 + k)) by A10, KURATO_0: 4;

            

             A13: x in (A1 . (n1 + (n2 + n3))) & not x in (A2 . (n1 + (n2 + n3))) or not x in (A1 . (n1 + (n2 + n3))) & x in (A2 . (n1 + (n2 + n3))) by A4;

            

             A14: x in (A2 . (n3 + (n1 + n2))) by A11;

            x in (A1 . (n2 + (n1 + n3))) by A12;

            hence contradiction by A14, A13;

          end;

        end;

      end;

      assume

       A15: A1 is convergent or A2 is convergent;

      per cases by A15;

        suppose A1 is convergent;

        hence thesis by A1;

      end;

        suppose A2 is convergent;

        hence thesis by A1;

      end;

    end;

    theorem :: SETLIM_2:66

    

     Th66: A1 is convergent & A2 is convergent implies ( lim_inf (A1 (\+\) A2)) = (( lim_inf A1) \+\ ( lim_inf A2))

    proof

      assume that

       A1: A1 is convergent and

       A2: A2 is convergent;

      thus ( lim_inf (A1 (\+\) A2)) c= (( lim_inf A1) \+\ ( lim_inf A2)) by A1, Th65;

      thus (( lim_inf A1) \+\ ( lim_inf A2)) c= ( lim_inf (A1 (\+\) A2))

      proof

        let x be object;

        assume

         A3: x in (( lim_inf A1) \+\ ( lim_inf A2));

        per cases by A3, XBOOLE_0: 1;

          suppose

           A4: x in ( lim_inf A1) & not x in ( lim_inf A2);

          then not x in ( lim_sup A2) by A2, KURATO_0:def 5;

          then

          consider n2 be Nat such that

           A5: for k holds not x in (A2 . (n2 + k)) by KURATO_0: 5;

          consider n1 be Nat such that

           A6: for k holds x in (A1 . (n1 + k)) by A4, KURATO_0: 4;

          now

            let k;

            x in (A1 . (n1 + (n2 + k))) & not x in (A2 . (n2 + (n1 + k))) by A6, A5;

            then x in ((A1 . ((n1 + n2) + k)) \+\ (A2 . ((n1 + n2) + k))) by XBOOLE_0: 1;

            hence x in ((A1 (\+\) A2) . ((n1 + n2) + k)) by Def4;

          end;

          hence thesis by KURATO_0: 4;

        end;

          suppose

           A7: not x in ( lim_inf A1) & x in ( lim_inf A2);

          then not x in ( lim_sup A1) by A1, KURATO_0:def 5;

          then

          consider n3 be Nat such that

           A8: for k holds not x in (A1 . (n3 + k)) by KURATO_0: 5;

          consider n4 be Nat such that

           A9: for k holds x in (A2 . (n4 + k)) by A7, KURATO_0: 4;

          now

            let k;

            ( not x in (A1 . (n3 + (n4 + k)))) & x in (A2 . (n4 + (n3 + k))) by A8, A9;

            then x in ((A1 . ((n3 + n4) + k)) \+\ (A2 . ((n3 + n4) + k))) by XBOOLE_0: 1;

            hence x in ((A1 (\+\) A2) . ((n3 + n4) + k)) by Def4;

          end;

          hence thesis by KURATO_0: 4;

        end;

      end;

    end;

    theorem :: SETLIM_2:67

    

     Th67: ( lim_sup (A1 (/\) A2)) c= (( lim_sup A1) /\ ( lim_sup A2))

    proof

      ((A1 (/\) A2) . n) = ((A1 . n) /\ (A2 . n)) by Def1;

      hence thesis by KURATO_0: 13;

    end;

    theorem :: SETLIM_2:68

    

     Th68: ( lim_sup (A1 (\/) A2)) = (( lim_sup A1) \/ ( lim_sup A2))

    proof

      ((A1 (\/) A2) . n) = ((A1 . n) \/ (A2 . n)) by Def2;

      hence thesis by KURATO_0: 11;

    end;

    theorem :: SETLIM_2:69

    

     Th69: (( lim_sup A1) \ ( lim_sup A2)) c= ( lim_sup (A1 (\) A2))

    proof

      let x be object;

      assume

       A1: x in (( lim_sup A1) \ ( lim_sup A2));

      then not x in ( lim_sup A2) by XBOOLE_0:def 5;

      then

      consider n1 be Nat such that

       A2: for k holds not x in (A2 . (n1 + k)) by KURATO_0: 5;

      assume not x in ( lim_sup (A1 (\) A2));

      then

      consider n2 be Nat such that

       A3: for k holds not x in ((A1 (\) A2) . (n2 + k)) by KURATO_0: 5;

       A4:

      now

        let k;

         not x in ((A1 (\) A2) . (n2 + k)) by A3;

        then not x in ((A1 . (n2 + k)) \ (A2 . (n2 + k))) by Def3;

        hence not x in (A1 . (n2 + k)) or x in (A2 . (n2 + k)) by XBOOLE_0:def 5;

      end;

      x in ( lim_sup A1) by A1, XBOOLE_0:def 5;

      then

      consider k1 be Nat such that

       A5: x in (A1 . ((n1 + n2) + k1)) by KURATO_0: 5;

      

       A6: x in (A1 . (n2 + (k1 + n1))) by A5;

       not x in (A2 . (n1 + (n2 + k1))) by A2;

      hence contradiction by A4, A6;

    end;

    theorem :: SETLIM_2:70

    (( lim_sup A1) \+\ ( lim_sup A2)) c= ( lim_sup (A1 (\+\) A2))

    proof

      let x be object;

      

       A1: for A1, A2 st x in ( lim_sup A1) & not x in ( lim_sup A2) holds x in ( lim_sup (A1 (\+\) A2))

      proof

        let A1, A2;

        assume that

         A2: x in ( lim_sup A1) and

         A3: not x in ( lim_sup A2);

        consider n1 be Nat such that

         A4: for k holds not x in (A2 . (n1 + k)) by A3, KURATO_0: 5;

        now

          let n;

          consider k1 be Nat such that

           A5: x in (A1 . ((n + n1) + k1)) by A2, KURATO_0: 5;

           not x in (A2 . (n1 + (n + k1))) by A4;

          then x in ((A1 . (n + (n1 + k1))) \+\ (A2 . (n + (n1 + k1)))) by A5, XBOOLE_0: 1;

          then x in ((A1 (\+\) A2) . (n + (n1 + k1))) by Def4;

          hence ex k st x in ((A1 (\+\) A2) . (n + k));

        end;

        hence thesis by KURATO_0: 5;

      end;

      assume

       A6: x in (( lim_sup A1) \+\ ( lim_sup A2));

      per cases by A6, XBOOLE_0: 1;

        suppose x in ( lim_sup A1) & not x in ( lim_sup A2);

        hence thesis by A1;

      end;

        suppose not x in ( lim_sup A1) & x in ( lim_sup A2);

        hence thesis by A1;

      end;

    end;

    theorem :: SETLIM_2:71

    

     Th71: A1 is convergent or A2 is convergent implies ( lim_sup (A1 (/\) A2)) = (( lim_sup A1) /\ ( lim_sup A2))

    proof

      

       A1: for A1, A2 st A1 is convergent holds ( lim_sup (A1 (/\) A2)) = (( lim_sup A1) /\ ( lim_sup A2))

      proof

        let A1, A2;

        assume

         A2: A1 is convergent;

        thus ( lim_sup (A1 (/\) A2)) c= (( lim_sup A1) /\ ( lim_sup A2)) by Th67;

        thus (( lim_sup A1) /\ ( lim_sup A2)) c= ( lim_sup (A1 (/\) A2))

        proof

          let x be object;

          assume

           A3: x in (( lim_sup A1) /\ ( lim_sup A2));

          then x in ( lim_sup A1) by XBOOLE_0:def 4;

          then x in ( lim_inf A1) by A2, KURATO_0:def 5;

          then

          consider n1 be Nat such that

           A4: for k holds x in (A1 . (n1 + k)) by KURATO_0: 4;

          

           A5: x in ( lim_sup A2) by A3, XBOOLE_0:def 4;

          now

            let n;

            consider k1 be Nat such that

             A6: x in (A2 . ((n + n1) + k1)) by A5, KURATO_0: 5;

            x in (A1 . (n1 + (n + k1))) by A4;

            then x in ((A1 . (n + (n1 + k1))) /\ (A2 . (n + (n1 + k1)))) by A6, XBOOLE_0:def 4;

            then x in ((A1 (/\) A2) . (n + (n1 + k1))) by Def1;

            hence ex k st x in ((A1 (/\) A2) . (n + k));

          end;

          hence thesis by KURATO_0: 5;

        end;

      end;

      assume

       A7: A1 is convergent or A2 is convergent;

      per cases by A7;

        suppose A1 is convergent;

        hence thesis by A1;

      end;

        suppose A2 is convergent;

        hence thesis by A1;

      end;

    end;

    theorem :: SETLIM_2:72

    

     Th72: A2 is convergent implies ( lim_sup (A1 (\) A2)) = (( lim_sup A1) \ ( lim_sup A2))

    proof

      assume

       A1: A2 is convergent;

      thus ( lim_sup (A1 (\) A2)) c= (( lim_sup A1) \ ( lim_sup A2))

      proof

        let x be object;

        assume

         A2: x in ( lim_sup (A1 (\) A2));

         A3:

        now

          let n;

          consider k1 be Nat such that

           A4: x in ((A1 (\) A2) . (n + k1)) by A2, KURATO_0: 5;

          x in ((A1 . (n + k1)) \ (A2 . (n + k1))) by A4, Def3;

          then x in (A1 . (n + k1)) & not x in (A2 . (n + k1)) by XBOOLE_0:def 5;

          hence ex k st x in (A1 . (n + k)) & not x in (A2 . (n + k));

        end;

        assume not x in (( lim_sup A1) \ ( lim_sup A2));

        then

         A5: not (x in ( lim_sup A1) & not x in ( lim_sup A2)) by XBOOLE_0:def 5;

        per cases by A1, A5, KURATO_0:def 5;

          suppose not x in ( lim_sup A1);

          then

          consider n1 be Nat such that

           A6: for k holds not x in (A1 . (n1 + k)) by KURATO_0: 5;

          ex k2 be Nat st x in (A1 . (n1 + k2)) & not x in (A2 . (n1 + k2)) by A3;

          hence contradiction by A6;

        end;

          suppose x in ( lim_inf A2);

          then

          consider n2 be Nat such that

           A7: for k holds x in (A2 . (n2 + k)) by KURATO_0: 4;

          ex k3 be Nat st x in (A1 . (n2 + k3)) & not x in (A2 . (n2 + k3)) by A3;

          hence contradiction by A7;

        end;

      end;

      thus thesis by Th69;

    end;

    theorem :: SETLIM_2:73

    

     Th73: A1 is convergent & A2 is convergent implies ( lim_sup (A1 (\+\) A2)) = (( lim_sup A1) \+\ ( lim_sup A2))

    proof

      assume that

       A1: A1 is convergent and

       A2: A2 is convergent;

      

      thus ( lim_sup (A1 (\+\) A2)) = ( lim_sup ((A1 (\) A2) (\/) (A2 (\) A1))) by Th3

      .= (( lim_sup (A1 (\) A2)) \/ ( lim_sup (A2 (\) A1))) by Th68

      .= ((( lim_sup A1) \ ( lim_sup A2)) \/ ( lim_sup (A2 (\) A1))) by A2, Th72

      .= (( lim_sup A1) \+\ ( lim_sup A2)) by A1, Th72;

    end;

    theorem :: SETLIM_2:74

    

     Th74: ( lim_inf (A (/\) A1)) = (A /\ ( lim_inf A1))

    proof

      reconsider X1 = ( inferior_setsequence A1) as SetSequence of X;

      reconsider X2 = ( inferior_setsequence (A (/\) A1)) as SetSequence of X;

      X2 = (A (/\) X1)

      proof

        let n be Element of NAT ;

        

        thus (X2 . n) = (A /\ (X1 . n)) by Th50

        .= ((A (/\) X1) . n) by Def5;

      end;

      then ( Union X2) = (A /\ ( Union X1)) by Th38;

      then ( lim_inf (A (/\) A1)) = (A /\ ( Union X1)) by SETLIM_1:def 4;

      hence thesis by SETLIM_1:def 4;

    end;

    theorem :: SETLIM_2:75

    

     Th75: ( lim_inf (A (\/) A1)) = (A \/ ( lim_inf A1))

    proof

      reconsider X1 = ( inferior_setsequence A1) as SetSequence of X;

      reconsider X2 = ( inferior_setsequence (A (\/) A1)) as SetSequence of X;

      X2 = (A (\/) X1)

      proof

        let n be Element of NAT ;

        

        thus (X2 . n) = (A \/ (X1 . n)) by Th51

        .= ((A (\/) X1) . n) by Def6;

      end;

      then ( Union X2) = (A \/ ( Union X1)) by Th39;

      then ( lim_inf (A (\/) A1)) = (A \/ ( Union X1)) by SETLIM_1:def 4;

      hence thesis by SETLIM_1:def 4;

    end;

    theorem :: SETLIM_2:76

    

     Th76: ( lim_inf (A (\) A1)) c= (A \ ( lim_inf A1))

    proof

      let x be object;

      assume x in ( lim_inf (A (\) A1));

      then

      consider n such that

       A1: for k holds x in ((A (\) A1) . (n + k)) by KURATO_0: 4;

       A2:

      now

        let k;

        x in ((A (\) A1) . (n + k)) by A1;

        then x in (A \ (A1 . (n + k))) by Def7;

        hence x in A & not x in (A1 . (n + k)) by XBOOLE_0:def 5;

      end;

       not x in ( lim_inf A1)

      proof

        assume x in ( lim_inf A1);

        then

        consider n1 be Nat such that

         A3: for k holds x in (A1 . (n1 + k)) by KURATO_0: 4;

        x in (A1 . (n1 + n)) by A3;

        hence contradiction by A2;

      end;

      hence thesis by A2, XBOOLE_0:def 5;

    end;

    theorem :: SETLIM_2:77

    

     Th77: ( lim_inf (A1 (\) A)) = (( lim_inf A1) \ A)

    proof

      reconsider X1 = ( inferior_setsequence A1) as SetSequence of X;

      reconsider X2 = ( inferior_setsequence (A1 (\) A)) as SetSequence of X;

      X2 = (X1 (\) A)

      proof

        let n be Element of NAT ;

        

        thus (X2 . n) = ((X1 . n) \ A) by Th53

        .= ((X1 (\) A) . n) by Def8;

      end;

      then ( Union X2) = (( Union X1) \ A) by Th41;

      then ( lim_inf (A1 (\) A)) = (( Union X1) \ A) by SETLIM_1:def 4;

      hence thesis by SETLIM_1:def 4;

    end;

    theorem :: SETLIM_2:78

    

     Th78: ( lim_inf (A (\+\) A1)) c= (A \+\ ( lim_inf A1))

    proof

      let x be object;

      assume x in ( lim_inf (A (\+\) A1));

      then

      consider n1 be Nat such that

       A1: for k holds x in ((A (\+\) A1) . (n1 + k)) by KURATO_0: 4;

       A2:

      now

        let k;

        x in ((A (\+\) A1) . (n1 + k)) by A1;

        then x in (A \+\ (A1 . (n1 + k))) by Def9;

        hence x in A & not x in (A1 . (n1 + k)) or not x in A & x in (A1 . (n1 + k)) by XBOOLE_0: 1;

      end;

      assume not x in (A \+\ ( lim_inf A1));

      then

       A3: not x in A & not x in ( lim_inf A1) or x in ( lim_inf A1) & x in A by XBOOLE_0: 1;

      per cases by A3, KURATO_0: 4;

        suppose

         A4: not x in A & not ex n st for k holds x in (A1 . (n + k));

        then ex k1 be Nat st not x in (A1 . (n1 + k1));

        hence contradiction by A2, A4;

      end;

        suppose

         A5: x in A & ex n st for k holds x in (A1 . (n + k));

        then

        consider n2 be Nat such that

         A6: for k holds x in (A1 . (n2 + k));

        x in (A1 . (n2 + n1)) by A6;

        hence contradiction by A2, A5;

      end;

    end;

    theorem :: SETLIM_2:79

    

     Th79: A1 is convergent implies ( lim_inf (A (\) A1)) = (A \ ( lim_inf A1))

    proof

      assume

       A1: A1 is convergent;

      thus ( lim_inf (A (\) A1)) c= (A \ ( lim_inf A1)) by Th76;

      thus (A \ ( lim_inf A1)) c= ( lim_inf (A (\) A1))

      proof

        let x be object;

        assume

         A2: x in (A \ ( lim_inf A1));

        then x in (A \ ( lim_sup A1)) by A1, KURATO_0:def 5;

        then not x in ( lim_sup A1) by XBOOLE_0:def 5;

        then

        consider n1 be Nat such that

         A3: for k holds not x in (A1 . (n1 + k)) by KURATO_0: 5;

        assume

         A4: not x in ( lim_inf (A (\) A1));

        

         A5: for n holds not x in A or ex k st x in (A1 . (n + k))

        proof

          let n;

          consider k such that

           A6: not x in ((A (\) A1) . (n + k)) by A4, KURATO_0: 4;

           not x in (A \ (A1 . (n + k))) by A6, Def7;

          then not (x in A & not x in (A1 . (n + k))) by XBOOLE_0:def 5;

          hence thesis;

        end;

        per cases by A5;

          suppose not x in A;

          hence contradiction by A2, XBOOLE_0:def 5;

        end;

          suppose ex k st x in (A1 . (n1 + k));

          hence contradiction by A3;

        end;

      end;

    end;

    theorem :: SETLIM_2:80

    

     Th80: A1 is convergent implies ( lim_inf (A (\+\) A1)) = (A \+\ ( lim_inf A1))

    proof

      assume

       A1: A1 is convergent;

      thus ( lim_inf (A (\+\) A1)) c= (A \+\ ( lim_inf A1)) by Th78;

      thus (A \+\ ( lim_inf A1)) c= ( lim_inf (A (\+\) A1))

      proof

        let x be object;

        assume

         A2: x in (A \+\ ( lim_inf A1));

        per cases by A2, XBOOLE_0: 1;

          suppose

           A3: x in A & not x in ( lim_inf A1);

          then not x in ( lim_sup A1) by A1, KURATO_0:def 5;

          then

          consider n1 be Nat such that

           A4: for k holds not x in (A1 . (n1 + k)) by KURATO_0: 5;

          now

            let k;

             not x in (A1 . (n1 + k)) by A4;

            then x in (A \+\ (A1 . (n1 + k))) by A3, XBOOLE_0: 1;

            hence x in ((A (\+\) A1) . (n1 + k)) by Def9;

          end;

          hence thesis by KURATO_0: 4;

        end;

          suppose

           A5: not x in A & x in ( lim_inf A1);

          then

          consider n2 be Nat such that

           A6: for k holds x in (A1 . (n2 + k)) by KURATO_0: 4;

          now

            let k;

            x in (A1 . (n2 + k)) by A6;

            then x in (A \+\ (A1 . (n2 + k))) by A5, XBOOLE_0: 1;

            hence x in ((A (\+\) A1) . (n2 + k)) by Def9;

          end;

          hence thesis by KURATO_0: 4;

        end;

      end;

    end;

    theorem :: SETLIM_2:81

    

     Th81: ( lim_sup (A (/\) A1)) = (A /\ ( lim_sup A1))

    proof

      reconsider X1 = ( superior_setsequence A1) as SetSequence of X;

      reconsider X2 = ( superior_setsequence (A (/\) A1)) as SetSequence of X;

      X2 = (A (/\) X1)

      proof

        let n be Element of NAT ;

        

        thus (X2 . n) = (A /\ (X1 . n)) by Th55

        .= ((A (/\) X1) . n) by Def5;

      end;

      then ( Intersection X2) = (A /\ ( Intersection X1)) by Th33;

      then ( lim_sup (A (/\) A1)) = (A /\ ( Intersection X1)) by SETLIM_1:def 5;

      hence thesis by SETLIM_1:def 5;

    end;

    theorem :: SETLIM_2:82

    

     Th82: ( lim_sup (A (\/) A1)) = (A \/ ( lim_sup A1))

    proof

      reconsider X1 = ( superior_setsequence A1) as SetSequence of X;

      reconsider X2 = ( superior_setsequence (A (\/) A1)) as SetSequence of X;

      X2 = (A (\/) X1)

      proof

        let n be Element of NAT ;

        

        thus (X2 . n) = (A \/ (X1 . n)) by Th56

        .= ((A (\/) X1) . n) by Def6;

      end;

      then ( Intersection X2) = (A \/ ( Intersection X1)) by Th34;

      then ( lim_sup (A (\/) A1)) = (A \/ ( Intersection X1)) by SETLIM_1:def 5;

      hence thesis by SETLIM_1:def 5;

    end;

    theorem :: SETLIM_2:83

    

     Th83: (A \ ( lim_sup A1)) c= ( lim_sup (A (\) A1))

    proof

      let x be object;

      assume

       A1: x in (A \ ( lim_sup A1));

      then not x in ( lim_sup A1) by XBOOLE_0:def 5;

      then

      consider n1 be Nat such that

       A2: for k holds not x in (A1 . (n1 + k)) by KURATO_0: 5;

      assume not x in ( lim_sup (A (\) A1));

      then

      consider n such that

       A3: for k holds not x in ((A (\) A1) . (n + k)) by KURATO_0: 5;

       A4:

      now

        let k;

         not x in ((A (\) A1) . (n + k)) by A3;

        then not x in (A \ (A1 . (n + k))) by Def7;

        hence not x in A or x in (A1 . (n + k)) by XBOOLE_0:def 5;

      end;

      per cases by A4;

        suppose not x in A;

        hence contradiction by A1, XBOOLE_0:def 5;

      end;

        suppose

         A5: x in (A1 . (n + k));

         not x in (A1 . (n1 + n)) by A2;

        hence contradiction by A5;

      end;

    end;

    theorem :: SETLIM_2:84

    

     Th84: ( lim_sup (A1 (\) A)) = (( lim_sup A1) \ A)

    proof

      reconsider X1 = ( superior_setsequence A1) as SetSequence of X;

      reconsider X2 = ( superior_setsequence (A1 (\) A)) as SetSequence of X;

      X2 = (X1 (\) A)

      proof

        let n be Element of NAT ;

        

        thus (X2 . n) = ((X1 . n) \ A) by Th58

        .= ((X1 (\) A) . n) by Def8;

      end;

      then ( Intersection X2) = (( Intersection X1) \ A) by Th36;

      then ( lim_sup (A1 (\) A)) = (( Intersection X1) \ A) by SETLIM_1:def 5;

      hence thesis by SETLIM_1:def 5;

    end;

    theorem :: SETLIM_2:85

    

     Th85: (A \+\ ( lim_sup A1)) c= ( lim_sup (A (\+\) A1))

    proof

      ((A (\+\) A1) . n) = (A \+\ (A1 . n)) by Def9;

      hence thesis by KURATO_0: 17;

    end;

    theorem :: SETLIM_2:86

    

     Th86: A1 is convergent implies ( lim_sup (A (\) A1)) = (A \ ( lim_sup A1))

    proof

      assume

       A1: A1 is convergent;

      thus ( lim_sup (A (\) A1)) c= (A \ ( lim_sup A1))

      proof

        let x be object;

        assume

         A2: x in ( lim_sup (A (\) A1));

        

         A3: for n holds ex k st x in A & not x in (A1 . (n + k))

        proof

          let n;

          consider k such that

           A4: x in ((A (\) A1) . (n + k)) by A2, KURATO_0: 5;

          x in (A \ (A1 . (n + k))) by A4, Def7;

          then x in A & not x in (A1 . (n + k)) by XBOOLE_0:def 5;

          hence thesis;

        end;

        

         A5: x in A

        proof

          

           A6: for n holds ex k st x in A

          proof

            let n;

            ex k st x in A & not x in (A1 . (n + k)) by A3;

            hence thesis;

          end;

          assume not x in A;

          then for n holds not x in A;

          hence contradiction by A6;

        end;

        for n holds ex k st not x in (A1 . (n + k))

        proof

          let n;

          ex k st x in A & not x in (A1 . (n + k)) by A3;

          hence thesis;

        end;

        then not x in ( lim_inf A1) by KURATO_0: 4;

        then not x in ( lim_sup A1) by A1, KURATO_0:def 5;

        hence thesis by A5, XBOOLE_0:def 5;

      end;

      thus thesis by Th83;

    end;

    theorem :: SETLIM_2:87

    

     Th87: A1 is convergent implies ( lim_sup (A (\+\) A1)) = (A \+\ ( lim_sup A1))

    proof

      assume

       A1: A1 is convergent;

      thus ( lim_sup (A (\+\) A1)) c= (A \+\ ( lim_sup A1))

      proof

        let x be object;

        assume

         A2: x in ( lim_sup (A (\+\) A1));

         A3:

        now

          let n;

          consider k1 be Nat such that

           A4: x in ((A (\+\) A1) . (n + k1)) by A2, KURATO_0: 5;

          x in (A \+\ (A1 . (n + k1))) by A4, Def9;

          then x in A & not x in (A1 . (n + k1)) or not x in A & x in (A1 . (n + k1)) by XBOOLE_0: 1;

          hence ex k st x in A & not x in (A1 . (n + k)) or not x in A & x in (A1 . (n + k));

        end;

        assume

         A5: not x in (A \+\ ( lim_sup A1));

        per cases by A5, XBOOLE_0: 1;

          suppose

           A6: not x in A & not x in ( lim_sup A1);

          then

          consider n1 be Nat such that

           A7: for k holds not x in (A1 . (n1 + k)) by KURATO_0: 5;

          ex k1 be Nat st (x in A & not x in (A1 . (n1 + k1)) or not x in A & x in (A1 . (n1 + k1))) by A3;

          hence contradiction by A6, A7;

        end;

          suppose

           A8: x in A & x in ( lim_sup A1);

          then x in ( lim_inf A1) by A1, KURATO_0:def 5;

          then

          consider n2 be Nat such that

           A9: for k holds x in (A1 . (n2 + k)) by KURATO_0: 4;

          ex k2 be Nat st (x in A & not x in (A1 . (n2 + k2)) or not x in A & x in (A1 . (n2 + k2))) by A3;

          hence contradiction by A8, A9;

        end;

      end;

      thus thesis by Th85;

    end;

    theorem :: SETLIM_2:88

    A1 is convergent & A2 is convergent implies (A1 (/\) A2) is convergent & ( lim (A1 (/\) A2)) = (( lim A1) /\ ( lim A2))

    proof

      assume that

       A1: A1 is convergent and

       A2: A2 is convergent;

      

       A3: ( lim_sup (A1 (/\) A2)) = (( lim A1) /\ ( lim A2)) by A1, Th71;

      ( lim_inf (A1 (/\) A2)) = (( lim_inf A1) /\ ( lim_inf A2)) by Th60

      .= (( lim A1) /\ ( lim_inf A2)) by A1, KURATO_0:def 5

      .= (( lim A1) /\ ( lim A2)) by A2, KURATO_0:def 5;

      hence thesis by A3, KURATO_0:def 5;

    end;

    theorem :: SETLIM_2:89

    A1 is convergent & A2 is convergent implies (A1 (\/) A2) is convergent & ( lim (A1 (\/) A2)) = (( lim A1) \/ ( lim A2))

    proof

      assume that

       A1: A1 is convergent and

       A2: A2 is convergent;

      

       A3: ( lim_sup (A1 (\/) A2)) = (( lim A1) \/ ( lim A2)) by Th68;

      ( lim_inf (A1 (\/) A2)) = (( lim_inf A1) \/ ( lim_inf A2)) by A1, Th63

      .= (( lim A1) \/ ( lim_inf A2)) by A1, KURATO_0:def 5

      .= (( lim A1) \/ ( lim A2)) by A2, KURATO_0:def 5;

      hence thesis by A3, KURATO_0:def 5;

    end;

    theorem :: SETLIM_2:90

    A1 is convergent & A2 is convergent implies (A1 (\) A2) is convergent & ( lim (A1 (\) A2)) = (( lim A1) \ ( lim A2))

    proof

      assume that

       A1: A1 is convergent and

       A2: A2 is convergent;

      

       A3: ( lim_sup (A1 (\) A2)) = (( lim A1) \ ( lim A2)) by A2, Th72;

      ( lim_inf (A1 (\) A2)) = (( lim_inf A1) \ ( lim_inf A2)) by A2, Th64

      .= (( lim A1) \ ( lim_inf A2)) by A1, KURATO_0:def 5

      .= (( lim A1) \ ( lim A2)) by A2, KURATO_0:def 5;

      hence thesis by A3, KURATO_0:def 5;

    end;

    theorem :: SETLIM_2:91

    A1 is convergent & A2 is convergent implies (A1 (\+\) A2) is convergent & ( lim (A1 (\+\) A2)) = (( lim A1) \+\ ( lim A2))

    proof

      assume that

       A1: A1 is convergent and

       A2: A2 is convergent;

      

       A3: ( lim_sup (A1 (\+\) A2)) = (( lim A1) \+\ ( lim A2)) by A1, A2, Th73;

      ( lim_inf (A1 (\+\) A2)) = (( lim_inf A1) \+\ ( lim_inf A2)) by A1, A2, Th66

      .= (( lim A1) \+\ ( lim_inf A2)) by A1, KURATO_0:def 5

      .= (( lim A1) \+\ ( lim A2)) by A2, KURATO_0:def 5;

      hence thesis by A3, KURATO_0:def 5;

    end;

    theorem :: SETLIM_2:92

    A1 is convergent implies (A (/\) A1) is convergent & ( lim (A (/\) A1)) = (A /\ ( lim A1))

    proof

      assume

       A1: A1 is convergent;

      

       A2: ( lim_inf (A (/\) A1)) = (A /\ ( lim_inf A1)) by Th74

      .= (A /\ ( lim A1)) by A1, KURATO_0:def 5;

      then ( lim_sup (A (/\) A1)) = ( lim_inf (A (/\) A1)) by Th81;

      hence thesis by A2, KURATO_0:def 5;

    end;

    theorem :: SETLIM_2:93

    A1 is convergent implies (A (\/) A1) is convergent & ( lim (A (\/) A1)) = (A \/ ( lim A1))

    proof

      assume

       A1: A1 is convergent;

      

       A2: ( lim_inf (A (\/) A1)) = (A \/ ( lim_inf A1)) by Th75

      .= (A \/ ( lim A1)) by A1, KURATO_0:def 5;

      then ( lim_sup (A (\/) A1)) = ( lim_inf (A (\/) A1)) by Th82;

      hence thesis by A2, KURATO_0:def 5;

    end;

    theorem :: SETLIM_2:94

    A1 is convergent implies (A (\) A1) is convergent & ( lim (A (\) A1)) = (A \ ( lim A1))

    proof

      assume

       A1: A1 is convergent;

      

      then

       A2: ( lim_inf (A (\) A1)) = (A \ ( lim_inf A1)) by Th79

      .= (A \ ( lim A1)) by A1, KURATO_0:def 5;

      then ( lim_sup (A (\) A1)) = ( lim_inf (A (\) A1)) by A1, Th86;

      hence thesis by A2, KURATO_0:def 5;

    end;

    theorem :: SETLIM_2:95

    A1 is convergent implies (A1 (\) A) is convergent & ( lim (A1 (\) A)) = (( lim A1) \ A)

    proof

      assume

       A1: A1 is convergent;

      

       A2: ( lim_inf (A1 (\) A)) = (( lim_inf A1) \ A) by Th77

      .= (( lim A1) \ A) by A1, KURATO_0:def 5;

      then ( lim_sup (A1 (\) A)) = ( lim_inf (A1 (\) A)) by Th84;

      hence thesis by A2, KURATO_0:def 5;

    end;

    theorem :: SETLIM_2:96

    A1 is convergent implies (A (\+\) A1) is convergent & ( lim (A (\+\) A1)) = (A \+\ ( lim A1))

    proof

      assume

       A1: A1 is convergent;

      

      then

       A2: ( lim_inf (A (\+\) A1)) = (A \+\ ( lim_inf A1)) by Th80

      .= (A \+\ ( lim A1)) by A1, KURATO_0:def 5;

      then ( lim_sup (A (\+\) A1)) = ( lim_inf (A (\+\) A1)) by A1, Th87;

      hence thesis by A2, KURATO_0:def 5;

    end;