setlim_1.miz

    begin

    reserve n,m,k,k1,k2,i,j for Nat;

    reserve x,y,z for object,

X,Y,Z for set;

    reserve A for Subset of X;

    reserve B,A1,A2,A3 for SetSequence of X;

    reserve Si for SigmaField of X;

    reserve S,S1,S2,S3 for SetSequence of Si;



     Lm1: for i,j be Nat holds i <= j implies i = j or (i + 1) <= j

    proof

      let i,j be Nat;

      assume i <= j;

      then (i + 1) <= (j + 1) by XREAL_1: 6;

      hence thesis by NAT_1: 8, XCMPLX_1: 2;

    end;

    theorem :: SETLIM_1:1



     Th1: for f be sequence of Y holds (f . (n + m)) in { (f . k) : n <= k }

    proof

      n <= (n + m) by NAT_1: 11;

      hence thesis;

    end;

    theorem :: SETLIM_1:2



     Th2: for f be sequence of Y holds { (f . k1) : n <= k1 } = ({ (f . k2) : (n + 1) <= k2 } \/ {(f . n)})

    proof

      let f be sequence of Y;

      set Z1 = { (f . k1) : n <= k1 };

      set Z2 = { (f . k2) : (n + 1) <= k2 };



       A1: (Z2 \/ {(f . n)}) c= Z1

      proof

        let x be object;

        assume

         A2: x in (Z2 \/ {(f . n)});

        now

          per cases by A2, XBOOLE_0:def 3;

            case x in Z2;

            then

            consider z such that

             A3: x = z and

             A4: z in Z2;

            consider k11 be Nat such that

             A5: z = (f . k11) and

             A6: (n + 1) <= k11 by A4;

            n <= k11 by A6, NAT_1: 13;

            hence thesis by A3, A5;

          end;

            case x in {(f . n)};

            then x = (f . n) by TARSKI:def 1;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      { (f . k1) : n <= k1 } c= ({ (f . k2) : (n + 1) <= k2 } \/ {(f . n)})

      proof

        let x be object;

        assume x in Z1;

        then

        consider z such that

         A7: x = z and

         A8: z in Z1;

        consider k such that

         A9: z = (f . k) & n <= k by A8;

        z = (f . k) & (n + 1) <= k or z = (f . k) & n = k by A9, Lm1;

        then z in Z2 or z in {(f . n)} by TARSKI:def 1;

        hence thesis by A7, XBOOLE_0:def 3;

      end;

      hence thesis by A1, XBOOLE_0:def 10;

    end;

    theorem :: SETLIM_1:3



     Th3: for f be sequence of Y holds (for k1 holds x in (f . (n + k1))) iff for Z st Z in { (f . k2) : n <= k2 } holds x in Z

    proof

      let f be sequence of Y;

      set Z = { (f . k2) : n <= k2 };

      now

        assume

         A1: for k1 holds x in (f . (n + k1));

        now

          let Z1 be set;

          assume Z1 in Z;

          then

          consider k1 be Nat such that

           A2: Z1 = (f . k1) and

           A3: n <= k1;

          ex m be Nat st k1 = (n + m) by A3, NAT_1: 10;

          then

          consider k2 be Nat such that

           A4: Z1 = (f . (n + k2)) by A2;

          thus x in Z1 by A1, A4;

        end;

        hence for Z1 be set st Z1 in { (f . k2) : n <= k2 } holds x in Z1;

      end;

      hence thesis by Th1;

    end;

    theorem :: SETLIM_1:4



     Th4: for Y be non empty set holds for f be sequence of Y holds x in ( rng f) iff ex n st x = (f . n)

    proof

      let Y be non empty set;

      let f be sequence of Y;

      thus x in ( rng f) implies ex n st x = (f . n)

      proof

        assume x in ( rng f);

        then

        consider y be object such that

         A1: y in ( dom f) and

         A2: x = (f . y) by FUNCT_1:def 3;

        reconsider m = y as Element of NAT by A1;

        take m;

        thus thesis by A2;

      end;

      given n such that

       A3: x = (f . n);



       A4: n in NAT by ORDINAL1:def 12;

      ( dom f) = NAT by FUNCT_2:def 1;

      hence thesis by A3, FUNCT_1:def 3, A4;

    end;

    theorem :: SETLIM_1:5



     Th5: for Y be non empty set holds for f be sequence of Y holds ( rng f) = { (f . k) : 0 <= k }

    proof

      let Y be non empty set;

      let f be sequence of Y;

      set Z = { (f . k) : 0 <= k };



       A1: ( dom f) = NAT by FUNCT_2:def 1;



       A2: ( rng f) c= Z

      proof

        let y be object;

        assume y in ( rng f);

        then

        consider n be object such that

         A3: n in NAT and

         A4: y = (f . n) by A1, FUNCT_1:def 3;

        reconsider n as Element of NAT by A3;

         0 <= n by NAT_1: 2;

        hence thesis by A4;

      end;

      Z c= ( rng f)

      proof

        let x be object;

        assume x in Z;

        then

        consider n1 be Nat such that

         A5: x = (f . n1) & 0 <= n1;

        n1 in NAT by ORDINAL1:def 12;

        hence thesis by FUNCT_2: 4, A5;

      end;

      hence thesis by A2, XBOOLE_0:def 10;

    end;

    theorem :: SETLIM_1:6



     Th6: for Y be non empty set holds for f be sequence of Y holds ( rng (f ^\ k)) = { (f . n) : k <= n }

    proof

      let Y be non empty set;

      let f be sequence of Y;

      reconsider f1 = (f ^\ k) as sequence of Y;

      ( rng f1) = { (f . m) : k <= m }

      proof

        set Z = { (f . m) : k <= m };



         A1: ( dom f1) = NAT by FUNCT_2:def 1;



         A2: ( rng f1) c= Z

        proof

          let y be object;

          assume y in ( rng f1);

          then

          consider m1 be object such that

           A3: m1 in NAT and

           A4: y = (f1 . m1) by A1, FUNCT_1:def 3;

          reconsider m1 as Element of NAT by A3;

          y = (f . (k + m1)) by A4, NAT_1:def 3;

          hence thesis by Th1;

        end;

        Z c= ( rng f1)

        proof

          let x be object;

          assume x in Z;

          then

          consider k1 be Nat such that

           A5: x = (f . k1) and

           A6: k <= k1;

          consider k2 be Nat such that

           A7: k1 = (k + k2) by A6, NAT_1: 10;

          k2 in NAT & x = (f1 . k2) by A5, A7, NAT_1:def 3, ORDINAL1:def 12;

          hence thesis by FUNCT_2: 4;

        end;

        hence thesis by A2, XBOOLE_0:def 10;

      end;

      hence thesis;

    end;

    theorem :: SETLIM_1:7



     Th7: x in ( meet ( rng B)) iff for n be Nat holds x in (B . n)

    proof



       A1: ( dom B) = NAT by FUNCT_2:def 1;

       A2:

      now

        let x;

        assume

         A3: for n be Nat holds x in (B . n);

        now

          let Y;

          assume Y in ( rng B);

          then

          consider n be object such that

           A4: n in NAT and

           A5: Y = (B . n) by A1, FUNCT_1:def 3;

          thus x in Y by A3, A4, A5;

        end;

        hence x in ( meet ( rng B)) by SETFAM_1:def 1;

      end;

      now

        let x;

        assume

         A6: x in ( meet ( rng B));

        now

          let k be Nat;

          k in NAT by ORDINAL1:def 12;

          then (B . k) in ( rng B) by FUNCT_2: 4;

          hence x in (B . k) by A6, SETFAM_1:def 1;

        end;

        hence for n be Nat holds x in (B . n);

      end;

      hence thesis by A2;

    end;

    theorem :: SETLIM_1:8



     Th8: ( Intersection B) = ( meet ( rng B))

    proof

      now

        let x be object;

        assume x in ( meet ( rng B));

        then for n be Nat holds x in (B . n) by Th7;

        hence x in ( Intersection B) by PROB_1: 13;

      end;

      then

       A1: ( meet ( rng B)) c= ( Intersection B);

      ( Intersection B) c= ( meet ( rng B))

      proof

        let x be object;

        assume x in ( Intersection B);

        then for n be Nat holds x in (B . n) by PROB_1: 13;

        hence thesis by Th7;

      end;

      hence thesis by A1, XBOOLE_0:def 10;

    end;

    theorem :: SETLIM_1:9

    ( Intersection B) c= ( Union B)

    proof

      ( meet ( rng B)) c= ( union ( rng B)) by SETFAM_1: 2;

      then ( Intersection B) c= ( union ( rng B)) by Th8;

      hence thesis by CARD_3:def 4;

    end;

    theorem :: SETLIM_1:10



     Th10: (for n holds (B . n) = A) implies ( Union B) = A

    proof

      assume

       A1: for n holds (B . n) = A;

      now

        let x be object;

        assume x in ( rng B);

        then ex n st x = (B . n) by Th4;

        hence x = A by A1;

      end;

      then ( rng B) = {A} by ZFMISC_1: 35;

      then ( union ( rng B)) = A by ZFMISC_1: 25;

      hence thesis by CARD_3:def 4;

    end;

    theorem :: SETLIM_1:11



     Th11: (for n holds (B . n) = A) implies ( Intersection B) = A

    proof

      assume

       A1: for n holds (B . n) = A;

      now

        let x be object;

        assume x in ( rng B);

        then ex n st x = (B . n) by Th4;

        hence x = A by A1;

      end;

      then ( rng B) = {A} by ZFMISC_1: 35;

      then ( meet ( rng B)) = A by SETFAM_1: 10;

      hence thesis by Th8;

    end;

    theorem :: SETLIM_1:12

    B is constant implies ( Union B) = ( Intersection B)

    proof

      assume B is constant;

      then

      consider A be Subset of X such that

       A1: for n be Nat holds (B . n) = A by VALUED_0:def 18;

      ( Union B) = A by Th10, A1;

      hence thesis by Th11, A1;

    end;



     Lm2: B is constant & ( the_value_of B) = A implies for n holds (B . n) = A & ( Union B) = A & ( Intersection B) = A

    proof

      assume that

       A1: B is constant and

       A2: ( the_value_of B) = A;

      consider x be set such that

       A3: x in ( dom B) and

       A4: A = (B . x) by A1, A2, FUNCT_1:def 12;



       A5: ( dom B) = NAT by FUNCT_2:def 1;

      for n holds (B . n) = A

      proof

        let n;

        reconsider n as Element of NAT by ORDINAL1:def 12;

        (B . n) = A by A1, A3, A4, FUNCT_1:def 10, A5;

        hence thesis;

      end;

      hence thesis by Th10, Th11;

    end;

    theorem :: SETLIM_1:13



     Th13: B is constant & ( the_value_of B) = A implies for n holds ( union { (B . k) : n <= k }) = A

    proof

      assume

       A1: B is constant & ( the_value_of B) = A;

      let n;

      set Y = { (B . k) : n <= k };

       A2:

      now

        let x be object;

        assume x in Y;

        then ex k st x = (B . k) & n <= k;

        hence x = A by A1, Lm2;

      end;

      Y <> {} by Th1;

      then Y = {A} by A2, ZFMISC_1: 35;

      hence thesis by ZFMISC_1: 25;

    end;

    theorem :: SETLIM_1:14



     Th14: B is constant & ( the_value_of B) = A implies for n holds ( meet { (B . k) : n <= k }) = A

    proof

      assume

       A1: B is constant & ( the_value_of B) = A;

      let n;

      set Y = { (B . k) : n <= k };

       A2:

      now

        let x be object;

        assume x in Y;

        then ex k st x = (B . k) & n <= k;

        hence x = A by A1, Lm2;

      end;

      Y <> {} by Th1;

      then Y = {A} by A2, ZFMISC_1: 35;

      hence thesis by SETFAM_1: 10;

    end;

    theorem :: SETLIM_1:15



     Th15: for X, B holds for f be Function st ( dom f) = NAT & for n holds (f . n) = ( meet { (B . k) : n <= k }) holds f is SetSequence of X

    proof

      let X, B;

      let f be Function such that

       A1: ( dom f) = NAT and

       A2: for n holds (f . n) = ( meet { (B . k) : n <= k });

      ( rng f) c= ( bool X)

      proof

        let z be object;

        assume z in ( rng f);

        then

        consider x be object such that

         A3: x in ( dom f) and

         A4: z = (f . x) by FUNCT_1:def 3;

        reconsider n = x as Element of NAT by A1, A3;

        set Y = { (B . k) : n <= k };

        set y = ( meet Y);



         A5: y is Subset of X

        proof

          per cases ;

            suppose Y <> {} ;

            then

            consider Z1 be object such that

             A6: Z1 in Y by XBOOLE_0:def 1;

            reconsider Z1 as set by TARSKI: 1;

            consider k1 be Nat such that

             A7: Z1 = (B . k1) & n <= k1 by A6;

            reconsider k1 as Element of NAT by ORDINAL1:def 12;

            now

              let x be object;

              assume x in y;

              then x in Z1 by A6, SETFAM_1:def 1;

              then x in (B . k1) by A7;

              hence x in X;

            end;

            hence thesis by TARSKI:def 3;

          end;

            suppose Y = {} ;

            then y = {} by SETFAM_1:def 1;

            hence thesis by XBOOLE_1: 2;

          end;

        end;

        z = y by A2, A4;

        hence thesis by A5;

      end;

      hence thesis by A1, FUNCT_2: 2;

    end;

    theorem :: SETLIM_1:16



     Th16: for X be set, B be SetSequence of X holds for f be Function st ( dom f) = NAT & for n holds (f . n) = ( union { (B . k) : n <= k }) holds f is sequence of ( bool X)

    proof

      let X be set, B be SetSequence of X;

      let f be Function such that

       A1: ( dom f) = NAT and

       A2: for n holds (f . n) = ( union { (B . k) : n <= k });

      ( rng f) c= ( bool X)

      proof

        let z be object;

        assume z in ( rng f);

        then

        consider x be object such that

         A3: x in ( dom f) and

         A4: z = (f . x) by FUNCT_1:def 3;

        reconsider n = x as Nat by A1, A3;

        set Y = { (B . k) : n <= k };

        set y = ( union Y);

        now

          let z be object;

          assume z in y;

          then ex Z st z in Z & Z in Y by TARSKI:def 4;

          then

          consider Z1 be set such that

           A5: Z1 in Y and

           A6: z in Z1;

          consider k1 such that

           A7: Z1 = (B . k1) & n <= k1 by A5;

          reconsider k1 as Element of NAT by ORDINAL1:def 12;

          Z1 = (B . k1) by A7;

          hence z in X by A6;

        end;

        then

         A8: y is Subset of X by TARSKI:def 3;

        z = y by A2, A4;

        hence thesis by A8;

      end;

      hence thesis by A1, FUNCT_2: 2;

    end;

    definition

      let X, B;

      :: SETLIM_1:def1

      attr B is monotone means B is non-descending or B is non-ascending;

    end

    definition

      let B be Function;

      :: SETLIM_1:def2

      func inferior_setsequence B -> Function means

      : Def2: ( dom it ) = NAT & for n holds (it . n) = ( meet { (B . k) : n <= k });

      existence

      proof

        deffunc F( Nat) = ( meet { (B . k) : $1 <= k });

        consider f be Function such that

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

        take f;

        thus ( dom f) = NAT by A1;

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let BSeq,CSeq be Function such that

         A2: ( dom BSeq) = NAT & for n holds (BSeq . n) = ( meet { (B . k) : n <= k }) and

         A3: ( dom CSeq) = NAT & for m holds (CSeq . m) = ( meet { (B . k) : m <= k });

        for y be object st y in NAT holds (BSeq . y) = (CSeq . y)

        proof

          let y be object;

          assume y in NAT ;

          then

          reconsider y as Nat;

          set Y = { (B . k) : y <= k };

          (BSeq . y) = ( meet Y) by A2;

          hence thesis by A3;

        end;

        hence thesis by A2, A3, FUNCT_1: 2;

      end;

    end

    definition

      let X be set, B be SetSequence of X;

      :: original: inferior_setsequence

      redefine

      func inferior_setsequence B -> SetSequence of X ;

      coherence

      proof



         A1: for n be Nat holds (( inferior_setsequence B) . n) = ( meet { (B . k) : n <= k }) by Def2;

        ( dom ( inferior_setsequence B)) = NAT by Def2;

        hence thesis by A1, Th15;

      end;

    end

    definition

      let B be Function;

      :: SETLIM_1:def3

      func superior_setsequence B -> Function means

      : Def3: ( dom it ) = NAT & for n holds (it . n) = ( union { (B . k) : n <= k });

      existence

      proof

        deffunc F( Nat) = ( union { (B . k) : $1 <= k });

        consider f be Function such that

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

        take f;

        thus ( dom f) = NAT by A1;

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let BSeq,CSeq be Function such that

         A2: ( dom BSeq) = NAT & for n holds (BSeq . n) = ( union { (B . k) : n <= k }) and

         A3: ( dom CSeq) = NAT & for m holds (CSeq . m) = ( union { (B . k) : m <= k });

        for y be object st y in NAT holds (BSeq . y) = (CSeq . y)

        proof

          let y be object;

          assume y in NAT ;

          then

          reconsider y as Nat;

          set Y = { (B . k) : y <= k };

          (BSeq . y) = ( union Y) by A2;

          hence thesis by A3;

        end;

        hence thesis by A2, A3, FUNCT_1: 2;

      end;

    end

    definition

      let X be set, B be SetSequence of X;

      :: original: superior_setsequence

      redefine

      func superior_setsequence B -> SetSequence of X ;

      coherence

      proof



         A1: for n holds (( superior_setsequence B) . n) = ( union { (B . k) : n <= k }) by Def3;

        ( dom ( superior_setsequence B)) = NAT by Def3;

        hence thesis by A1, Th16;

      end;

    end

    theorem :: SETLIM_1:17



     Th17: (( inferior_setsequence B) . 0 ) = ( Intersection B)

    proof

      (( inferior_setsequence B) . 0 ) = ( meet { (B . k) : k >= 0 }) by Def2

      .= ( meet ( rng B)) by Th5

      .= ( Intersection B) by Th8;

      hence thesis;

    end;

    theorem :: SETLIM_1:18



     Th18: (( superior_setsequence B) . 0 ) = ( Union B)

    proof

      (( superior_setsequence B) . 0 ) = ( union { (B . k) : 0 <= k }) by Def3

      .= ( union ( rng B)) by Th5

      .= ( Union B) by CARD_3:def 4;

      hence thesis;

    end;

    theorem :: SETLIM_1:19



     Th19: for n be Nat holds x in (( inferior_setsequence B) . n) iff for k be Nat holds x in (B . (n + k))

    proof

      let n be Nat;

      reconsider nn = n as Nat;

      set Y = { (B . k) : nn <= k };



       A1: (( inferior_setsequence B) . n) = ( meet { (B . k) : n <= k }) by Def2;

       A2:

      now

        assume

         A3: x in (( inferior_setsequence B) . n);

        now

          let k be Nat;

          (B . (n + k)) in Y by Th1;

          hence x in (B . (n + k)) by A1, A3, SETFAM_1:def 1;

        end;

        hence for k be Nat holds x in (B . (n + k));

      end;



       A4: Y <> {} by Th1;

      now

        assume for k holds x in (B . (n + k));

        then for Z st Z in Y holds x in Z by Th3;

        hence x in (( inferior_setsequence B) . n) by A1, A4, SETFAM_1:def 1;

      end;

      hence thesis by A2;

    end;

    theorem :: SETLIM_1:20



     Th20: for n be Nat holds x in (( superior_setsequence B) . n) iff ex k be Nat st x in (B . (n + k))

    proof

      let n be Nat;

      set Y = { (B . k) : n <= k };



       A1: (( superior_setsequence B) . n) = ( union { (B . k) : n <= k }) by Def3;

      thus x in (( superior_setsequence B) . n) implies ex k be Nat st x in (B . (n + k))

      proof

        assume x in (( superior_setsequence B) . n);

        then

        consider Y1 be set such that

         A2: x in Y1 and

         A3: Y1 in Y by A1, TARSKI:def 4;

        consider k11 be Nat such that

         A4: Y1 = (B . k11) and

         A5: n <= k11 by A3;

        ex k be Nat st k11 = (n + k) by A5, NAT_1: 10;

        then

        consider k22 be Nat such that

         A6: Y1 = (B . (n + k22)) by A4;

        thus thesis by A2, A6;

      end;

      now

        given k1 be Nat such that

         A7: x in (B . (n + k1));

        (B . (n + k1)) in Y by Th1;

        hence x in (( superior_setsequence B) . n) by A1, A7, TARSKI:def 4;

      end;

      hence thesis;

    end;

    theorem :: SETLIM_1:21



     Th21: for n be Nat holds (( inferior_setsequence B) . n) = ((( inferior_setsequence B) . (n + 1)) /\ (B . n))

    proof

      let n be Nat;



       A1: (( inferior_setsequence B) . n) = ( meet { (B . k1) : n <= k1 }) by Def2;



       A2: { (B . k1) : n <= k1 } = ({ (B . k2) : (n + 1) <= k2 } \/ {(B . n)}) by Th2;



       A3: (( inferior_setsequence B) . (n + 1)) = ( meet { (B . k2) : (n + 1) <= k2 }) by Def2;



       A4: { (B . k1) : n <= k1 } <> {} by Th1;

       A5:

      now

        let x be object;

        assume that

         A6: x in (( inferior_setsequence B) . (n + 1)) and

         A7: x in (B . n);

        for Z st Z in { (B . k2) : n <= k2 } holds x in Z

        proof

          let Z;

          assume Z in { (B . k1) : n <= k1 };

          then

          consider Z1 be set such that

           A8: Z = Z1 & Z1 in { (B . k1) : n <= k1 };

          consider k11 be Nat such that

           A9: Z1 = (B . k11) & n <= k11 by A8;

          now

            per cases by A9, Lm1;

              suppose Z1 = (B . k11) & n = k11;

              hence x in Z1 by A7;

            end;

              suppose Z1 = (B . k11) & (n + 1) <= k11;

              then Z1 in { (B . k2) : (n + 1) <= k2 };

              hence x in Z1 by A3, A6, SETFAM_1:def 1;

            end;

          end;

          hence thesis by A8;

        end;

        then x in ( meet { (B . k2) : n <= k2 }) by A4, SETFAM_1:def 1;

        hence x in (( inferior_setsequence B) . n) by Def2;

      end;

      { (B . k2) : (n + 1) <= k2 } <> {} by Th1;

      then

       A10: (( inferior_setsequence B) . n) c= (( inferior_setsequence B) . (n + 1)) by A1, A3, A2, SETFAM_1: 6, XBOOLE_1: 7;

      now

        let x be object;



         A11: (B . n) in { (B . k1) : n <= k1 };

        assume x in (( inferior_setsequence B) . n);

        hence x in (( inferior_setsequence B) . (n + 1)) & x in (B . n) by A1, A10, A11, SETFAM_1:def 1;

      end;

      hence (( inferior_setsequence B) . n) = ((( inferior_setsequence B) . (n + 1)) /\ (B . n)) by A5, XBOOLE_0:def 4;

    end;

    theorem :: SETLIM_1:22



     Th22: for n be Nat holds (( superior_setsequence B) . n) = ((( superior_setsequence B) . (n + 1)) \/ (B . n))

    proof

      let n be Nat;

      { (B . k1) : n <= k1 } = ({ (B . k2) : (n + 1) <= k2 } \/ {(B . n)}) by Th2;

      then ( union { (B . k2) : (n + 1) <= k2 }) c= ( union { (B . k1) : n <= k1 }) by XBOOLE_1: 7, ZFMISC_1: 77;

      then (( superior_setsequence B) . (n + 1)) c= ( union { (B . k1) : n <= k1 }) by Def3;

      then

       A1: (( superior_setsequence B) . (n + 1)) c= (( superior_setsequence B) . n) by Def3;

       A2:

      now

        let x be object;

        assume

         A3: x in (( superior_setsequence B) . (n + 1)) or x in (B . n);

        thus x in (( superior_setsequence B) . n)

        proof

          now

            per cases by A3;

              case x in (( superior_setsequence B) . (n + 1));

              hence thesis by A1;

            end;

              case

               A4: x in (B . n);

              (B . n) in { (B . k1) : n <= k1 };

              then x in ( union { (B . k1) : n <= k1 }) by A4, TARSKI:def 4;

              hence thesis by Def3;

            end;

          end;

          hence thesis;

        end;

      end;

      now

        let x be object;

        assume x in (( superior_setsequence B) . n);

        then x in ( union { (B . k1) : n <= k1 }) by Def3;

        then

        consider Y1 be set such that

         A5: x in Y1 & Y1 in { (B . k1) : n <= k1 } by TARSKI:def 4;

        consider k11 be Nat such that

         A6: Y1 = (B . k11) & n <= k11 by A5;

        now

          per cases by A6, Lm1;

            case Y1 = (B . k11) & n = k11;

            hence x in (B . n) by A5;

          end;

            case Y1 = (B . k11) & (n + 1) <= k11;

            then Y1 in { (B . k2) : (n + 1) <= k2 };

            hence x in ( union { (B . k2) : (n + 1) <= k2 }) by A5, TARSKI:def 4;

          end;

        end;

        hence x in (B . n) or x in (( superior_setsequence B) . (n + 1)) by Def3;

      end;

      then for x be object holds x in (( superior_setsequence B) . n) iff x in (B . n) or x in (( superior_setsequence B) . (n + 1)) by A2;

      hence (( superior_setsequence B) . n) = ((( superior_setsequence B) . (n + 1)) \/ (B . n)) by XBOOLE_0:def 3;

    end;

    theorem :: SETLIM_1:23



     Th23: ( inferior_setsequence B) is non-descending

    proof

      now

        let n be Nat;

        (( inferior_setsequence B) . n) = ((( inferior_setsequence B) . (n + 1)) /\ (B . n)) by Th21;

        hence (( inferior_setsequence B) . n) c= (( inferior_setsequence B) . (n + 1)) by XBOOLE_1: 17;

      end;

      hence thesis by PROB_2: 7;

    end;

    theorem :: SETLIM_1:24



     Th24: ( superior_setsequence B) is non-ascending

    proof

      now

        let n be Nat;

        (( superior_setsequence B) . n) = ((( superior_setsequence B) . (n + 1)) \/ (B . n)) by Th22;

        hence (( superior_setsequence B) . (n + 1)) c= (( superior_setsequence B) . n) by XBOOLE_1: 7;

      end;

      hence thesis by PROB_2: 6;

    end;

    theorem :: SETLIM_1:25

    ( inferior_setsequence B) is monotone & ( superior_setsequence B) is monotone by Th23, Th24;

    registration

      let X be set, A be SetSequence of X;

      cluster ( inferior_setsequence A) -> non-descending;

      coherence by Th23;

    end

    registration

      let X be set, A be SetSequence of X;

      cluster ( superior_setsequence A) -> non-ascending;

      coherence by Th24;

    end

    theorem :: SETLIM_1:26

    ( Intersection B) c= (( inferior_setsequence B) . n)

    proof

       0 <= n by NAT_1: 2;

      then (( inferior_setsequence B) . 0 ) c= (( inferior_setsequence B) . n) by PROB_1:def 5;

      hence thesis by Th17;

    end;

    theorem :: SETLIM_1:27

    (( superior_setsequence B) . n) c= ( Union B)

    proof

       0 <= n by NAT_1: 2;

      then (( superior_setsequence B) . n) c= (( superior_setsequence B) . 0 ) by PROB_1:def 4;

      hence thesis by Th18;

    end;

    theorem :: SETLIM_1:28



     Th28: for B, n holds { (B . k) : n <= k } is Subset-Family of X

    proof

      let B, n;

      set Y1 = { (B . k) : n <= k };

      Y1 c= ( bool X)

      proof

        let x be object;

        assume x in Y1;

        then

        consider k such that

         A1: x = (B . k) & n <= k;

        reconsider k as Element of NAT by ORDINAL1:def 12;

        x = (B . k) by A1;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: SETLIM_1:29

    ( Union B) = (( Intersection ( Complement B)) ` )

    proof

      (( Intersection ( Complement B)) ` ) = ((( Union ( Complement ( Complement B))) ` ) ` ) by PROB_1:def 3

      .= ( Union B);

      hence thesis;

    end;

    theorem :: SETLIM_1:30



     Th30: for n be Element of NAT holds (( inferior_setsequence B) . n) = ((( superior_setsequence ( Complement B)) . n) ` )

    proof

      let n be Element of NAT ;

      set Y1 = { (B . k1) : n <= k1 };

      set Y2 = { (( Complement B) . k2) : n <= k2 };

      set Y3 = { ((B . k) ` ) where k be Element of NAT : n <= k };



       A1: Y3 c= Y2

      proof

        let y be object;

        assume y in Y3;

        then

        consider k be Element of NAT such that

         A2: y = ((B . k) ` ) and

         A3: n <= k;

        y = (( Complement B) . k) by A2, PROB_1:def 2;

        hence thesis by A3;

      end;

      Y2 c= Y3

      proof

        let x be object;

        assume x in Y2;

        then

        consider k such that

         A4: x = (( Complement B) . k) and

         A5: n <= k;

        reconsider k as Element of NAT by ORDINAL1:def 12;

        x = ((B . k) ` ) by A4, PROB_1:def 2;

        hence thesis by A5;

      end;

      then

       A6: Y2 = Y3 by A1, XBOOLE_0:def 10;



       A7: Y1 <> {} by Th1;

      reconsider Y1 as Subset-Family of X by Th28;



       A8: ( COMPLEMENT Y1) c= Y3

      proof

        let y be object;

        assume

         A9: y in ( COMPLEMENT Y1);

        then

        reconsider y as Subset of X;

        (y ` ) in Y1 by A9, SETFAM_1:def 7;

        then

        consider k such that

         A10: (y ` ) = (B . k) and

         A11: n <= k;

        reconsider k as Element of NAT by ORDINAL1:def 12;

        y = ((B . k) ` ) by A10;

        hence thesis by A11;

      end;

      Y3 c= ( COMPLEMENT Y1)

      proof

        let x be object;

        assume x in Y3;

        then

        consider k be Element of NAT such that

         A12: x = ((B . k) ` ) and

         A13: n <= k;

        reconsider z = (B . k) as Subset of X;

        ((z ` ) ` ) in Y1 by A13;

        hence thesis by A12, SETFAM_1:def 7;

      end;

      then Y3 = ( COMPLEMENT Y1) by A8, XBOOLE_0:def 10;



      then (( superior_setsequence ( Complement B)) . n) = ( union ( COMPLEMENT Y1)) by A6, Def3

      .= (( [#] X) \ ( meet Y1)) by A7, SETFAM_1: 34

      .= (( meet Y1) ` );

      hence thesis by Def2;

    end;

    theorem :: SETLIM_1:31

    for n be Element of NAT holds (( superior_setsequence B) . n) = ((( inferior_setsequence ( Complement B)) . n) ` )

    proof

      let n be Element of NAT ;

      reconsider Y = (( inferior_setsequence ( Complement B)) . n) as Subset of X;

      Y = ((( superior_setsequence ( Complement ( Complement B))) . n) ` ) by Th30

      .= ((( superior_setsequence B) . n) ` );

      hence thesis;

    end;

    theorem :: SETLIM_1:32



     Th32: ( Complement ( inferior_setsequence B)) = ( superior_setsequence ( Complement B))

    proof

      reconsider A2 = ( inferior_setsequence B) as SetSequence of X;

      reconsider A3 = ( superior_setsequence ( Complement B)) as SetSequence of X;

      now

        let n be Element of NAT ;

        ((A2 . n) ` ) = (((A3 . n) ` ) ` ) by Th30;

        hence (( Complement A2) . n) = (A3 . n) by PROB_1:def 2;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: SETLIM_1:33

    ( Complement ( superior_setsequence B)) = ( inferior_setsequence ( Complement B))

    proof

      reconsider A2 = ( inferior_setsequence ( Complement B)) as SetSequence of X;

      ( Complement A2) = ( superior_setsequence ( Complement ( Complement B))) by Th32

      .= ( superior_setsequence B);

      hence thesis;

    end;

    theorem :: SETLIM_1:34

    (for n be Nat holds (A3 . n) = ((A1 . n) \/ (A2 . n))) implies for n be Nat holds ((( inferior_setsequence A1) . n) \/ (( inferior_setsequence A2) . n)) c= (( inferior_setsequence A3) . n)

    proof

      assume

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

      let n be Nat;

      set X1 = ( inferior_setsequence A1), X2 = ( inferior_setsequence A2), X3 = ( inferior_setsequence A3);

      now

        let x be object;

        assume

         A2: x in ((X1 . n) \/ (X2 . n));

        per cases by A2, XBOOLE_0:def 3;

          suppose

           A3: x in (X1 . n);

          now

            let k be Nat;

            x in (A1 . (n + k)) & (A3 . (n + k)) = ((A1 . (n + k)) \/ (A2 . (n + k))) by A1, A3, Th19;

            hence x in (A3 . (n + k)) by XBOOLE_0:def 3;

          end;

          hence x in (X3 . n) by Th19;

        end;

          suppose

           A4: x in (X2 . n);

          now

            let k be Nat;

            x in (A2 . (n + k)) & (A3 . (n + k)) = ((A1 . (n + k)) \/ (A2 . (n + k))) by A1, A4, Th19;

            hence x in (A3 . (n + k)) by XBOOLE_0:def 3;

          end;

          hence x in (X3 . n) by Th19;

        end;

      end;

      hence thesis;

    end;

    theorem :: SETLIM_1:35

    (for n be Nat holds (A3 . n) = ((A1 . n) /\ (A2 . n))) implies for n be Nat holds (( inferior_setsequence A3) . n) = ((( inferior_setsequence A1) . n) /\ (( inferior_setsequence A2) . n))

    proof

      assume

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

      let n be Nat;

      reconsider X3 = ( inferior_setsequence A3) as SetSequence of X;

      reconsider X2 = ( inferior_setsequence A2) as SetSequence of X;

      set B = A1;

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



       A2: ((X1 . n) /\ (X2 . n)) c= (X3 . n)

      proof

        let x be object;

        assume x in ((X1 . n) /\ (X2 . n));

        then

         A3: x in (X1 . n) & x in (X2 . n) by XBOOLE_0:def 4;

        now

          let k be Nat;

          x in (B . (n + k)) & x in (A2 . (n + k)) by A3, Th19;

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

          hence x in (A3 . (n + k)) by A1;

        end;

        hence thesis by Th19;

      end;

      (X3 . n) c= ((X1 . n) /\ (X2 . n))

      proof

        let x be object;

        assume

         A4: x in (X3 . n);

        now

          let k be Nat;

          x in (A3 . (n + k)) by A4, Th19;

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

          hence x in (B . (n + k)) & x in (A2 . (n + k)) by XBOOLE_0:def 4;

        end;

        then x in (X1 . n) & x in (X2 . n) by Th19;

        hence thesis by XBOOLE_0:def 4;

      end;

      hence thesis by A2, XBOOLE_0:def 10;

    end;

    theorem :: SETLIM_1:36

    (for n holds (A3 . n) = ((A1 . n) \/ (A2 . n))) implies for n holds (( superior_setsequence A3) . n) = ((( superior_setsequence A1) . n) \/ (( superior_setsequence A2) . n))

    proof

      assume

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

      let n;

      reconsider X3 = ( superior_setsequence A3) as SetSequence of X;

      reconsider X2 = ( superior_setsequence A2) as SetSequence of X;

      set B = A1;

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



       A2: ((X1 . n) \/ (X2 . n)) c= (X3 . n)

      proof

        let x be object;

        assume

         A3: x in ((X1 . n) \/ (X2 . n));

        per cases by A3, XBOOLE_0:def 3;

          suppose x in (X1 . n);

          then

          consider k be Nat such that

           A4: x in (B . (n + k)) by Th20;

          (A3 . (n + k)) = ((B . (n + k)) \/ (A2 . (n + k))) by A1;

          then x in (A3 . (n + k)) by A4, XBOOLE_0:def 3;

          hence thesis by Th20;

        end;

          suppose x in (X2 . n);

          then

          consider k be Nat such that

           A5: x in (A2 . (n + k)) by Th20;

          (A3 . (n + k)) = ((B . (n + k)) \/ (A2 . (n + k))) by A1;

          then x in (A3 . (n + k)) by A5, XBOOLE_0:def 3;

          hence thesis by Th20;

        end;

      end;

      (X3 . n) c= ((X1 . n) \/ (X2 . n))

      proof

        let x be object;

        assume x in (X3 . n);

        then

        consider k be Nat such that

         A6: x in (A3 . (n + k)) by Th20;



         A7: x in ((B . (n + k)) \/ (A2 . (n + k))) by A1, A6;

        now

          per cases by A7, XBOOLE_0:def 3;

            case x in (B . (n + k));

            hence x in (X1 . n) by Th20;

          end;

            case x in (A2 . (n + k));

            hence x in (X2 . n) by Th20;

          end;

        end;

        hence thesis by XBOOLE_0:def 3;

      end;

      hence thesis by A2, XBOOLE_0:def 10;

    end;

    theorem :: SETLIM_1:37

    (for n holds (A3 . n) = ((A1 . n) /\ (A2 . n))) implies for n holds (( superior_setsequence A3) . n) c= ((( superior_setsequence A1) . n) /\ (( superior_setsequence A2) . n))

    proof

      assume

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

      let n;

      reconsider X3 = ( superior_setsequence A3) as SetSequence of X;

      reconsider X2 = ( superior_setsequence A2) as SetSequence of X;

      set B = A1;

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

      (X3 . n) c= ((X1 . n) /\ (X2 . n))

      proof

        let x be object;

        assume x in (X3 . n);

        then

        consider k be Nat such that

         A2: x in (A3 . (n + k)) by Th20;



         A3: (A3 . (n + k)) = ((B . (n + k)) /\ (A2 . (n + k))) by A1;

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

        then

         A4: x in (X2 . n) by Th20;

        x in (B . (n + k)) by A2, A3, XBOOLE_0:def 4;

        then x in (X1 . n) by Th20;

        hence thesis by A4, XBOOLE_0:def 4;

      end;

      hence thesis;

    end;

    theorem :: SETLIM_1:38



     Th38: B is constant & ( the_value_of B) = A implies for n holds (( inferior_setsequence B) . n) = A

    proof

      assume

       A1: B is constant & ( the_value_of B) = A;

      let n;

      (( inferior_setsequence B) . n) = ( meet { (B . k) : n <= k }) by Def2;

      hence thesis by A1, Th14;

    end;

    theorem :: SETLIM_1:39



     Th39: B is constant & ( the_value_of B) = A implies for n holds (( superior_setsequence B) . n) = A

    proof

      assume

       A1: B is constant & ( the_value_of B) = A;

      let n;

      (( superior_setsequence B) . n) = ( union { (B . k) : n <= k }) by Def3;

      hence thesis by A1, Th13;

    end;

    theorem :: SETLIM_1:40



     Th40: for n be Nat holds B is non-descending implies (B . n) c= (( superior_setsequence B) . (n + 1))

    proof

      let n be Nat;

      assume B is non-descending;

      then

       A1: (B . n) c= (B . (n + 1)) by PROB_2: 7;

      (B . n) c= ( union { (B . k) : (n + 1) <= k })

      proof

        let x be object;



         A2: (B . (n + 1)) in { (B . k) : (n + 1) <= k };

        assume x in (B . n);

        hence thesis by A1, A2, TARSKI:def 4;

      end;

      hence thesis by Def3;

    end;

    theorem :: SETLIM_1:41



     Th41: for n be Nat holds B is non-descending implies (( superior_setsequence B) . n) = (( superior_setsequence B) . (n + 1))

    proof

      let n be Nat;

      assume B is non-descending;

      then ((( superior_setsequence B) . (n + 1)) \/ (B . n)) = (( superior_setsequence B) . (n + 1)) by Th40, XBOOLE_1: 12;

      hence thesis by Th22;

    end;

    theorem :: SETLIM_1:42



     Th42: for n be Nat holds B is non-descending implies (( superior_setsequence B) . n) = ( Union B)

    proof

      let n be Nat;

      defpred P[ Nat] means (( superior_setsequence B) . $1) = ( Union B);

      assume B is non-descending;

      then

       A1: for k be Nat st P[k] holds P[(k + 1)] by Th41;



       A2: P[ 0 ] by Th18;

      for k be Nat holds P[k] from NAT_1:sch 2( A2, A1);

      hence thesis;

    end;

    theorem :: SETLIM_1:43



     Th43: B is non-descending implies ( Intersection ( superior_setsequence B)) = ( Union B)

    proof

      assume

       A1: B is non-descending;

      now

        let x be object;

        assume

         A2: x in ( Intersection ( superior_setsequence B));

        now

          let n;

          (( superior_setsequence B) . n) = ( Union B) by A1, Th42;

          hence x in ( Union B) by A2, PROB_1: 13;

        end;

        hence x in ( Union B);

      end;

      then

       A3: ( Intersection ( superior_setsequence B)) c= ( Union B);

      now

        let y be object;

        assume y in ( Union B);

        then for n be Nat holds y in (( superior_setsequence B) . n) by A1, Th42;

        hence y in ( Intersection ( superior_setsequence B)) by PROB_1: 13;

      end;

      then ( Union B) c= ( Intersection ( superior_setsequence B));

      hence thesis by A3, XBOOLE_0:def 10;

    end;

    theorem :: SETLIM_1:44



     Th44: B is non-descending implies (B . n) c= (( inferior_setsequence B) . (n + 1))

    proof

      set Y = { (B . k) : (n + 1) <= k };

      assume

       A1: B is non-descending;

      let x be object;

      assume

       A2: x in (B . n);

       A3:

      now

        let y be set;

        assume y in Y;

        then

        consider k1 be Nat such that

         A4: y = (B . k1) and

         A5: (n + 1) <= k1;

        n <= k1 by A5, NAT_1: 13;

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

        hence x in y by A2, A4;

      end;



       A6: Y <> {} by Th1;

      (( inferior_setsequence B) . (n + 1)) = ( meet { (B . k) : (n + 1) <= k }) by Def2;

      hence thesis by A6, A3, SETFAM_1:def 1;

    end;

    theorem :: SETLIM_1:45



     Th45: B is non-descending implies (( inferior_setsequence B) . n) = (B . n)

    proof

      assume B is non-descending;

      then ((( inferior_setsequence B) . (n + 1)) /\ (B . n)) = (B . n) by Th44, XBOOLE_1: 28;

      hence thesis by Th21;

    end;

    theorem :: SETLIM_1:46



     Th46: B is non-descending implies ( inferior_setsequence B) = B

    proof

      assume B is non-descending;

      then (( inferior_setsequence B) . n) = (B . n) by Th45;

      then for n be Element of NAT holds (( inferior_setsequence B) . n) = (B . n);

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: SETLIM_1:47



     Th47: B is non-ascending implies (( superior_setsequence B) . (n + 1)) c= (B . n)

    proof

      assume

       A1: B is non-ascending;

      let x be object;

      assume x in (( superior_setsequence B) . (n + 1));

      then

      consider k be Nat such that

       A2: x in (B . ((n + 1) + k)) by Th20;

      (n + 1) <= ((n + 1) + k) by NAT_1: 11;

      then n <= ((n + 1) + k) by NAT_1: 13;

      then (B . ((n + 1) + k)) c= (B . n) by A1, PROB_1:def 4;

      hence thesis by A2;

    end;

    theorem :: SETLIM_1:48



     Th48: B is non-ascending implies (( superior_setsequence B) . n) = (B . n)

    proof

      assume B is non-ascending;

      then ((( superior_setsequence B) . (n + 1)) \/ (B . n)) = (B . n) by Th47, XBOOLE_1: 12;

      hence thesis by Th22;

    end;

    theorem :: SETLIM_1:49



     Th49: B is non-ascending implies ( superior_setsequence B) = B

    proof

      assume B is non-ascending;

      then (( superior_setsequence B) . n) = (B . n) by Th48;

      then for n be Element of NAT holds (( superior_setsequence B) . n) = (B . n);

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: SETLIM_1:50



     Th50: for n be Nat holds B is non-ascending implies (( inferior_setsequence B) . (n + 1)) c= (B . n)

    proof

      let n be Nat;

      set Y = { (B . k) : (n + 1) <= k };

      assume B is non-ascending;

      then

       A1: (B . (n + 1)) c= (B . n) by PROB_2: 6;



       A2: (B . (n + 1)) in Y;

       A3:

      now

        let x be object;

        assume x in ( meet Y);

        then x in (B . (n + 1)) by A2, SETFAM_1:def 1;

        hence x in (B . n) by A1;

      end;

      (( inferior_setsequence B) . (n + 1)) = ( meet { (B . k) : (n + 1) <= k }) by Def2;

      hence thesis by A3;

    end;

    theorem :: SETLIM_1:51



     Th51: for n be Nat holds B is non-ascending implies (( inferior_setsequence B) . n) = (( inferior_setsequence B) . (n + 1))

    proof

      let n be Nat;

      assume B is non-ascending;

      then ((( inferior_setsequence B) . (n + 1)) /\ (B . n)) = (( inferior_setsequence B) . (n + 1)) by Th50, XBOOLE_1: 28;

      hence thesis by Th21;

    end;

    theorem :: SETLIM_1:52



     Th52: for n be Nat holds B is non-ascending implies (( inferior_setsequence B) . n) = ( Intersection B)

    proof

      let n be Nat;

      defpred P[ Nat] means (( inferior_setsequence B) . $1) = ( Intersection B);

      assume B is non-ascending;

      then

       A1: for k be Nat st P[k] holds P[(k + 1)] by Th51;



       A2: P[ 0 ] by Th17;

      for k be Nat holds P[k] from NAT_1:sch 2( A2, A1);

      hence thesis;

    end;

    theorem :: SETLIM_1:53



     Th53: B is non-ascending implies ( Union ( inferior_setsequence B)) = ( Intersection B)

    proof

      assume

       A1: B is non-ascending;

      now

        let x be object;

        assume x in ( Union ( inferior_setsequence B));

        then ex k be Nat st x in (( inferior_setsequence B) . k) by PROB_1: 12;

        hence x in ( Intersection B) by A1, Th52;

      end;

      then

       A2: ( Union ( inferior_setsequence B)) c= ( Intersection B);

      now

        let y be object;

        assume y in ( Intersection B);

        then y in (( inferior_setsequence B) . 0 ) by Th17;

        hence y in ( Union ( inferior_setsequence B)) by PROB_1: 12;

      end;

      then ( Intersection B) c= ( Union ( inferior_setsequence B));

      hence thesis by A2, XBOOLE_0:def 10;

    end;

    definition

      let X be set, B be SetSequence of X;

      :: original: lim_inf

      redefine

      :: SETLIM_1:def4

      func lim_inf B equals ( Union ( inferior_setsequence B));

      compatibility

      proof

        let F be Subset of X;

        hereby

          assume

           A1: F = ( lim_inf B);

          for x be object holds x in F iff x in ( Union ( inferior_setsequence B))

          proof

            let x be object;

            hereby

              assume x in F;

              then

              consider n be Nat such that

               A2: for k be Nat holds x in (B . (n + k)) by A1, KURATO_0: 4;

              x in (( inferior_setsequence B) . n) by A2, Th19;

              hence x in ( Union ( inferior_setsequence B)) by PROB_1: 12;

            end;

            assume x in ( Union ( inferior_setsequence B));

            then

            consider n be Nat such that

             A3: x in (( inferior_setsequence B) . n) by PROB_1: 12;

            for k be Nat holds x in (B . (n + k)) by A3, Th19;

            hence thesis by A1, KURATO_0: 4;

          end;

          hence F = ( Union ( inferior_setsequence B)) by TARSKI: 2;

        end;

        assume

         A4: F = ( Union ( inferior_setsequence B));

        for x be object holds x in F iff x in ( lim_inf B)

        proof

          let x be object;

          hereby

            assume x in F;

            then

            consider n be Nat such that

             A5: x in (( inferior_setsequence B) . n) by A4, PROB_1: 12;

            for k be Nat holds x in (B . (n + k)) by A5, Th19;

            hence x in ( lim_inf B) by KURATO_0: 4;

          end;

          assume x in ( lim_inf B);

          then

          consider n be Nat such that

           A6: for k be Nat holds x in (B . (n + k)) by KURATO_0: 4;

          x in (( inferior_setsequence B) . n) by A6, Th19;

          hence thesis by A4, PROB_1: 12;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    definition

      let X be set, B be SetSequence of X;

      :: original: lim_sup

      redefine

      :: SETLIM_1:def5

      func lim_sup B equals ( Intersection ( superior_setsequence B));

      compatibility

      proof

        let F be Subset of X;

        hereby

          assume

           A1: F = ( lim_sup B);

          for x be object holds x in F iff x in ( Intersection ( superior_setsequence B))

          proof

            let x be object;

            hereby

              assume

               A2: x in F;

              for m be Nat holds x in (( superior_setsequence B) . m)

              proof

                let m be Nat;

                ex k be Nat st x in (B . (m + k)) by A1, A2, KURATO_0: 5;

                hence thesis by Th20;

              end;

              hence x in ( Intersection ( superior_setsequence B)) by PROB_1: 13;

            end;

            assume

             A3: x in ( Intersection ( superior_setsequence B));

            now

              let m be Nat;

              x in (( superior_setsequence B) . m) by A3, PROB_1: 13;

              hence ex k be Nat st x in (B . (m + k)) by Th20;

            end;

            hence thesis by A1, KURATO_0: 5;

          end;

          hence F = ( Intersection ( superior_setsequence B)) by TARSKI: 2;

        end;

        assume

         A4: F = ( Intersection ( superior_setsequence B));

        for x be object holds x in F iff x in ( lim_sup B)

        proof

          let x be object;

          hereby

            assume

             A5: x in F;

            now

              let m be Nat;

              x in (( superior_setsequence B) . m) by A4, A5, PROB_1: 13;

              hence ex k be Nat st x in (B . (m + k)) by Th20;

            end;

            hence x in ( lim_sup B) by KURATO_0: 5;

          end;

          assume

           A6: x in ( lim_sup B);

          for m be Nat holds x in (( superior_setsequence B) . m)

          proof

            let m be Nat;

            ex k be Nat st x in (B . (m + k)) by A6, KURATO_0: 5;

            hence thesis by Th20;

          end;

          hence thesis by A4, PROB_1: 13;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    notation

      let X be set, B be SetSequence of X;

      synonym lim B for lim_sup B;

    end

    theorem :: SETLIM_1:54

    ( Intersection B) c= ( lim_inf B)

    proof

      let x be object;

      assume x in ( Intersection B);

      then for k be Nat holds x in (B . ( 0 + k)) by PROB_1: 13;

      hence thesis by KURATO_0: 4;

    end;

    theorem :: SETLIM_1:55

    ( lim_inf B) = ( lim ( inferior_setsequence B)) by Th43;

    theorem :: SETLIM_1:56

    ( lim_sup B) = ( lim ( superior_setsequence B)) by Th49;

    theorem :: SETLIM_1:57

    ( lim_sup B) = (( lim_inf ( Complement B)) ` )

    proof

      ( lim_inf ( Complement B)) = (( lim_sup ( Complement ( Complement B))) ` ) by KURATO_0: 9

      .= (( lim_sup B) ` );

      hence thesis;

    end;

    theorem :: SETLIM_1:58



     Th58: B is constant & ( the_value_of B) = A implies B is convergent & ( lim B) = A & ( lim_inf B) = A & ( lim_sup B) = A

    proof

      assume

       A1: B is constant & ( the_value_of B) = A;

      then for n holds (( superior_setsequence B) . n) = A by Th39;

      then

       A2: ( lim_sup B) = A by Th11;

      for n holds (( inferior_setsequence B) . n) = A by A1, Th38;

      then ( lim_inf B) = A by Th10;

      hence thesis by A2, KURATO_0:def 5;

    end;

    theorem :: SETLIM_1:59

    B is non-descending implies ( lim_sup B) = ( Union B) by Th43;

    theorem :: SETLIM_1:60

    B is non-descending implies ( lim_inf B) = ( Union B) by Th46;

    theorem :: SETLIM_1:61

    B is non-ascending implies ( lim_sup B) = ( Intersection B) by Th49;

    theorem :: SETLIM_1:62

    B is non-ascending implies ( lim_inf B) = ( Intersection B) by Th53;

    theorem :: SETLIM_1:63



     Th63: B is non-descending implies B is convergent & ( lim B) = ( Union B)

    proof

      assume

       A1: B is non-descending;

      then ( lim_sup B) = ( Union B) & ( lim_inf B) = ( Union B) by Th43, Th46;

      hence B is convergent by KURATO_0:def 5;

      thus thesis by A1, Th43;

    end;

    theorem :: SETLIM_1:64



     Th64: B is non-ascending implies B is convergent & ( lim B) = ( Intersection B)

    proof

      assume

       A1: B is non-ascending;

      then ( lim_sup B) = ( Intersection B) & ( lim_inf B) = ( Intersection B) by Th49, Th53;

      hence B is convergent by KURATO_0:def 5;

      thus thesis by A1, Th49;

    end;

    theorem :: SETLIM_1:65

    B is monotone implies B is convergent

    proof

      assume

       A1: B is monotone;

      per cases by A1;

        suppose B is non-ascending;

        hence thesis by Th64;

      end;

        suppose B is non-descending;

        hence thesis by Th63;

      end;

    end;

    definition

      let X be set, Si be SigmaField of X, S be SetSequence of Si;

      :: original: inferior_setsequence

      redefine

      func inferior_setsequence S -> SetSequence of Si ;

      coherence

      proof

        now

          let n be Nat;

          reconsider DSeq = (S ^\ n) as SetSequence of X;

          reconsider n1 = n as Nat;

          for m be Nat holds (DSeq . m) in Si

          proof

            let m be Nat;

            (DSeq . m) = (S . (m + n1)) & (S . (m + n1)) in ( rng S) by NAT_1: 51, NAT_1:def 3;

            hence thesis;

          end;

          then ( rng DSeq) c= Si by NAT_1: 52;

          then

           A1: ( Intersection DSeq) in Si by PROB_1:def 6;

          ( Intersection DSeq) = ( meet ( rng DSeq)) by Th8;

          then ( Intersection DSeq) = ( meet { (S . k) : n1 <= k }) by Th6;

          hence (( inferior_setsequence S) . n) in Si by A1, Def2;

        end;

        then ( rng ( inferior_setsequence S)) c= Si by NAT_1: 52;

        hence thesis by RELAT_1:def 19;

      end;

    end

    definition

      let X be set, Si be SigmaField of X, S be SetSequence of Si;

      :: original: superior_setsequence

      redefine

      func superior_setsequence S -> SetSequence of Si ;

      coherence

      proof

        now

          let n be Nat;

          reconsider DSeq = (S ^\ n) as SetSequence of X;

          reconsider n1 = n as Nat;



           A1: ( Union DSeq) in Si by PROB_1: 17;

          ( Union DSeq) = ( union ( rng DSeq)) by CARD_3:def 4;

          then ( Union DSeq) = ( union { (S . k) : n1 <= k }) by Th6;

          hence (( superior_setsequence S) . n) in Si by A1, Def3;

        end;

        then ( rng ( superior_setsequence S)) c= Si by NAT_1: 52;

        hence thesis by RELAT_1:def 19;

      end;

    end

    theorem :: SETLIM_1:66



     Th66: x in ( lim_sup S) iff for n be Nat holds ex k be Nat st x in (S . (n + k))

    proof

      x in ( Intersection ( superior_setsequence B)) iff for n be Nat holds ex k be Nat st x in (B . (n + k))

      proof

        ( lim_sup B) = ( Intersection ( superior_setsequence B));

        hence thesis by KURATO_0: 5;

      end;

      hence thesis;

    end;

    theorem :: SETLIM_1:67



     Th67: x in ( lim_inf S) iff ex n be Nat st for k be Nat holds x in (S . (n + k))

    proof

      x in ( Union ( inferior_setsequence B)) iff ex n be Nat st for k be Nat holds x in (B . (n + k))

      proof

        ( lim_inf B) = ( Union ( inferior_setsequence B));

        hence thesis by KURATO_0: 4;

      end;

      hence thesis;

    end;

    theorem :: SETLIM_1:68

    ( Intersection S) c= ( lim_inf S)

    proof

      let x be object;

      assume x in ( Intersection S);

      then for k be Nat holds x in (S . ( 0 + k)) by PROB_1: 13;

      hence thesis by Th67;

    end;

    theorem :: SETLIM_1:69

    ( lim_sup S) c= ( Union S)

    proof

      let x be object;

      assume x in ( lim_sup S);

      then ex k be Nat st x in (S . ( 0 + k)) by Th66;

      hence thesis by PROB_1: 12;

    end;

    theorem :: SETLIM_1:70

    ( lim_inf S) c= ( lim_sup S)

    proof

      ( Union ( inferior_setsequence B)) c= ( Intersection ( superior_setsequence B))

      proof

        ( lim_inf B) = ( Union ( inferior_setsequence B)) & ( lim_sup B) = ( Intersection ( superior_setsequence B));

        hence thesis by KURATO_0: 6;

      end;

      hence thesis;

    end;

    theorem :: SETLIM_1:71



     Th71: ( lim_inf S) = (( lim_sup ( Complement S)) ` )

    proof

      ( Union ( inferior_setsequence B)) = (( Intersection ( superior_setsequence ( Complement B))) ` )

      proof

        ( lim_inf B) = ( Union ( inferior_setsequence B)) & (( lim_sup ( Complement B)) ` ) = (( Intersection ( superior_setsequence ( Complement B))) ` );

        hence thesis by KURATO_0: 9;

      end;

      hence thesis;

    end;

    theorem :: SETLIM_1:72

    ( lim_sup S) = (( lim_inf ( Complement S)) ` )

    proof

      ( lim_inf ( Complement S) qua non empty SetSequence of X) = (( lim_sup ( Complement ( Complement S))) ` ) by Th71

      .= (( lim_sup S) ` );

      hence thesis;

    end;

    theorem :: SETLIM_1:73

    (for n be Nat holds (S3 . n) = ((S1 . n) \/ (S2 . n))) implies (( lim_inf S1) \/ ( lim_inf S2)) c= ( lim_inf S3)

    proof



       A1: (for n be Nat holds (A3 . n) = ((B . n) \/ (A2 . n))) implies (( Union ( inferior_setsequence B)) \/ ( Union ( inferior_setsequence A2))) c= ( Union ( inferior_setsequence A3))

      proof



         A2: ( lim_inf B) = ( Union ( inferior_setsequence B)) & ( lim_inf A2) = ( Union ( inferior_setsequence A2));



         A3: ( lim_inf A3) = ( Union ( inferior_setsequence A3));

        assume for n be Nat holds (A3 . n) = ((B . n) \/ (A2 . n));

        hence thesis by A2, A3, KURATO_0: 12;

      end;

      assume for n be Nat holds (S3 . n) = ((S1 . n) \/ (S2 . n));

      hence thesis by A1;

    end;

    theorem :: SETLIM_1:74

    (for n be Nat holds (S3 . n) = ((S1 . n) /\ (S2 . n))) implies ( lim_inf S3) = (( lim_inf S1) /\ ( lim_inf S2))

    proof



       A1: (for n be Nat holds (A3 . n) = ((B . n) /\ (A2 . n))) implies (( Union ( inferior_setsequence B)) /\ ( Union ( inferior_setsequence A2))) = ( Union ( inferior_setsequence A3))

      proof



         A2: ( lim_inf B) = ( Union ( inferior_setsequence B)) & ( lim_inf A2) = ( Union ( inferior_setsequence A2));



         A3: ( lim_inf A3) = ( Union ( inferior_setsequence A3));

        assume for n be Nat holds (A3 . n) = ((B . n) /\ (A2 . n));

        hence thesis by A2, A3, KURATO_0: 10;

      end;

      assume for n be Nat holds (S3 . n) = ((S1 . n) /\ (S2 . n));

      hence thesis by A1;

    end;

    theorem :: SETLIM_1:75

    (for n be Nat holds (S3 . n) = ((S1 . n) \/ (S2 . n))) implies ( lim_sup S3) = (( lim_sup S1) \/ ( lim_sup S2))

    proof



       A1: (for n be Nat holds (A3 . n) = ((B . n) \/ (A2 . n))) implies (( Intersection ( superior_setsequence B)) \/ ( Intersection ( superior_setsequence A2))) = ( Intersection ( superior_setsequence A3))

      proof



         A2: ( lim_sup B) = ( Intersection ( superior_setsequence B)) & ( lim_sup A2) = ( Intersection ( superior_setsequence A2));



         A3: ( lim_sup A3) = ( Intersection ( superior_setsequence A3));

        assume for n be Nat holds (A3 . n) = ((B . n) \/ (A2 . n));

        hence thesis by A2, A3, KURATO_0: 11;

      end;

      assume for n be Nat holds (S3 . n) = ((S1 . n) \/ (S2 . n));

      hence thesis by A1;

    end;

    theorem :: SETLIM_1:76

    (for n be Nat holds (S3 . n) = ((S1 . n) /\ (S2 . n))) implies ( lim_sup S3) c= (( lim_sup S1) /\ ( lim_sup S2))

    proof



       A1: (for n be Nat holds (A3 . n) = ((B . n) /\ (A2 . n))) implies ( Intersection ( superior_setsequence A3)) c= (( Intersection ( superior_setsequence B)) /\ ( Intersection ( superior_setsequence A2)))

      proof



         A2: ( lim_sup B) = ( Intersection ( superior_setsequence B)) & ( lim_sup A2) = ( Intersection ( superior_setsequence A2));



         A3: ( lim_sup A3) = ( Intersection ( superior_setsequence A3));

        assume for n be Nat holds (A3 . n) = ((B . n) /\ (A2 . n));

        hence thesis by A2, A3, KURATO_0: 13;

      end;

      assume for n be Nat holds (S3 . n) = ((S1 . n) /\ (S2 . n));

      hence thesis by A1;

    end;

    theorem :: SETLIM_1:77

    S is constant & ( the_value_of S) = A implies S is convergent & ( lim S) = A & ( lim_inf S) = A & ( lim_sup S) = A

    proof



       A1: B is constant & ( the_value_of B) = A implies ( Union ( inferior_setsequence B)) = A & ( Intersection ( superior_setsequence B)) = A

      proof



         A2: ( lim_inf B) = ( Union ( inferior_setsequence B)) & ( lim_sup B) = ( Intersection ( superior_setsequence B));

        assume B is constant & ( the_value_of B) = A;

        hence thesis by A2, Th58;

      end;

      assume S is constant & ( the_value_of S) = A;

      then ( lim_inf S) = A & ( lim_sup S) = A by A1;

      hence thesis by KURATO_0:def 5;

    end;

    theorem :: SETLIM_1:78



     Th78: S is non-descending implies ( lim_sup S) = ( Union S) by Th43;

    theorem :: SETLIM_1:79



     Th79: S is non-descending implies ( lim_inf S) = ( Union S) by Th46;

    theorem :: SETLIM_1:80



     Th80: S is non-descending implies S is convergent & ( lim S) = ( Union S)

    proof

      assume

       A1: S is non-descending;

      then ( lim_sup S) = ( Union S) & ( lim_inf S) = ( Union S) by Th78, Th79;

      hence S is convergent by KURATO_0:def 5;

      thus thesis by A1, Th78;

    end;

    theorem :: SETLIM_1:81



     Th81: S is non-ascending implies ( lim_sup S) = ( Intersection S) by Th49;

    theorem :: SETLIM_1:82



     Th82: S is non-ascending implies ( lim_inf S) = ( Intersection S) by Th53;

    theorem :: SETLIM_1:83



     Th83: S is non-ascending implies S is convergent & ( lim S) = ( Intersection S)

    proof

      assume

       A1: S is non-ascending;

      then ( lim_sup S) = ( Intersection S) & ( lim_inf S) = ( Intersection S) by Th81, Th82;

      hence S is convergent by KURATO_0:def 5;

      thus thesis by A1, Th81;

    end;

    theorem :: SETLIM_1:84

    S is monotone implies S is convergent

    proof

      assume

       A1: S is monotone;

      per cases by A1;

        suppose S is non-ascending;

        hence thesis by Th83;

      end;

        suppose S is non-descending;

        hence thesis by Th80;

      end;

    end;