yellow15.miz



    begin

    scheme :: YELLOW15:sch1

    SeqLambda1C { i() -> Nat , D() -> non empty set , C[ object], F,G( object) -> set } :

ex p be FinSequence of D() st ( len p) = i() & for i be Nat st i in ( Seg i()) holds (C[i] implies (p . i) = F(i)) & ( not C[i] implies (p . i) = G(i))

      provided

       A1: for i be Nat st i in ( Seg i()) holds (C[i] implies F(i) in D()) & ( not C[i] implies G(i) in D());

      

       A2: for x be object st x in ( Seg i()) holds (C[x] implies F(x) in D()) & ( not C[x] implies G(x) in D()) by A1;

      consider p be Function of ( Seg i()), D() such that

       A3: for x be object st x in ( Seg i()) holds (C[x] implies (p . x) = F(x)) & ( not C[x] implies (p . x) = G(x)) from FUNCT_2:sch 5( A2);

      

       A4: ( dom p) = ( Seg i()) by FUNCT_2:def 1;

      then

      reconsider p as FinSequence by FINSEQ_1:def 2;

      ( rng p) c= D() by RELAT_1:def 19;

      then

      reconsider p as FinSequence of D() by FINSEQ_1:def 4;

      take p;

      i() is Element of NAT by ORDINAL1:def 12;

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

    end;

    begin

    definition

      let X be set;

      let p be FinSequence of ( bool X);

      let q be FinSequence of BOOLEAN ;

      :: YELLOW15:def1

      func MergeSequence (p,q) -> FinSequence of ( bool X) means

      : Def1: ( len it ) = ( len p) & for i be Nat st i in ( dom p) holds (it . i) = ( IFEQ ((q . i), TRUE ,(p . i),(X \ (p . i))));

      existence

      proof

        deffunc F( Nat) = ( IFEQ ((q . $1), TRUE ,(p . $1),(X \ (p . $1))));

        consider r be FinSequence such that

         A1: ( len r) = ( len p) and

         A2: for i be Nat st i in ( dom r) holds (r . i) = F(i) from FINSEQ_1:sch 2;

        ( rng r) c= ( bool X)

        proof

          let z be object;

          assume z in ( rng r);

          then

          consider i be Nat such that

           A3: i in ( dom r) and

           A4: (r . i) = z by FINSEQ_2: 10;

          

           A5: z = ( IFEQ ((q . i), TRUE ,(p . i),(X \ (p . i)))) by A2, A3, A4;

          i in ( Seg ( len p)) by A1, A3, FINSEQ_1:def 3;

          then

           A6: i in ( dom p) by FINSEQ_1:def 3;

          now

            per cases ;

              suppose (q . i) = TRUE ;

              then z = (p . i) by A5, FUNCOP_1:def 8;

              hence thesis by A6, FINSEQ_2: 11;

            end;

              suppose (q . i) <> TRUE ;

              then z = (X \ (p . i)) by A5, FUNCOP_1:def 8;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

        then

        reconsider r as FinSequence of ( bool X) by FINSEQ_1:def 4;

        take r;

        ( dom p) = ( dom r) by A1, FINSEQ_3: 29;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        let r1,r2 be FinSequence of ( bool X) such that

         A7: ( len r1) = ( len p) and

         A8: for i be Nat st i in ( dom p) holds (r1 . i) = ( IFEQ ((q . i), TRUE ,(p . i),(X \ (p . i)))) and

         A9: ( len r2) = ( len p) and

         A10: for i be Nat st i in ( dom p) holds (r2 . i) = ( IFEQ ((q . i), TRUE ,(p . i),(X \ (p . i))));

        

         A11: ( dom r1) = ( Seg ( len p)) by A7, FINSEQ_1:def 3;

        now

          let i be Nat;

          assume i in ( dom r1);

          then

           A12: i in ( dom p) by A11, FINSEQ_1:def 3;

          

          hence (r1 . i) = ( IFEQ ((q . i), TRUE ,(p . i),(X \ (p . i)))) by A8

          .= (r2 . i) by A10, A12;

        end;

        hence thesis by A7, A9, FINSEQ_2: 9;

      end;

    end

    ::$Canceled

    theorem :: YELLOW15:4

    

     Th1: for X be set holds for p be FinSequence of ( bool X) holds for q be FinSequence of BOOLEAN holds ( dom ( MergeSequence (p,q))) = ( dom p)

    proof

      let X be set;

      let p be FinSequence of ( bool X);

      let q be FinSequence of BOOLEAN ;

      

      thus ( dom ( MergeSequence (p,q))) = ( Seg ( len ( MergeSequence (p,q)))) by FINSEQ_1:def 3

      .= ( Seg ( len p)) by Def1

      .= ( dom p) by FINSEQ_1:def 3;

    end;

    theorem :: YELLOW15:5

    

     Th2: for X be set holds for p be FinSequence of ( bool X) holds for q be FinSequence of BOOLEAN holds for i be Nat st (q . i) = TRUE holds (( MergeSequence (p,q)) . i) = (p . i)

    proof

      let X be set;

      let p be FinSequence of ( bool X);

      let q be FinSequence of BOOLEAN ;

      let i be Nat;

      assume

       A1: (q . i) = TRUE ;

      now

        per cases ;

          suppose i in ( dom p);

          

          hence (( MergeSequence (p,q)) . i) = ( IFEQ ((q . i), TRUE ,(p . i),(X \ (p . i)))) by Def1

          .= (p . i) by A1, FUNCOP_1:def 8;

        end;

          suppose

           A2: not i in ( dom p);

          ( dom p) = ( Seg ( len p)) by FINSEQ_1:def 3

          .= ( Seg ( len ( MergeSequence (p,q)))) by Def1

          .= ( dom ( MergeSequence (p,q))) by FINSEQ_1:def 3;

          

          hence (( MergeSequence (p,q)) . i) = {} by A2, FUNCT_1:def 2

          .= (p . i) by A2, FUNCT_1:def 2;

        end;

      end;

      hence thesis;

    end;

    theorem :: YELLOW15:6

    

     Th3: for X be set holds for p be FinSequence of ( bool X) holds for q be FinSequence of BOOLEAN holds for i be Nat st i in ( dom p) & (q . i) = FALSE holds (( MergeSequence (p,q)) . i) = (X \ (p . i))

    proof

      let X be set;

      let p be FinSequence of ( bool X);

      let q be FinSequence of BOOLEAN ;

      let i be Nat;

      assume that

       A1: i in ( dom p) and

       A2: (q . i) = FALSE ;

      

      thus (( MergeSequence (p,q)) . i) = ( IFEQ ((q . i), TRUE ,(p . i),(X \ (p . i)))) by A1, Def1

      .= (X \ (p . i)) by A2, FUNCOP_1:def 8;

    end;

    theorem :: YELLOW15:7

    for X be set holds for q be FinSequence of BOOLEAN holds ( len ( MergeSequence (( <*> ( bool X)),q))) = 0

    proof

      let X be set;

      let q be FinSequence of BOOLEAN ;

      

      thus ( len ( MergeSequence (( <*> ( bool X)),q))) = ( len ( <*> ( bool X))) by Def1

      .= 0 ;

    end;

    theorem :: YELLOW15:8

    

     Th5: for X be set holds for q be FinSequence of BOOLEAN holds ( MergeSequence (( <*> ( bool X)),q)) = ( <*> ( bool X))

    proof

      let X be set;

      let q be FinSequence of BOOLEAN ;

      ( len ( MergeSequence (( <*> ( bool X)),q))) = ( len ( <*> ( bool X))) by Def1

      .= 0 ;

      hence thesis;

    end;

    theorem :: YELLOW15:9

    for X be set holds for x be Subset of X holds for q be FinSequence of BOOLEAN holds ( len ( MergeSequence ( <*x*>,q))) = 1

    proof

      let X be set;

      let x be Subset of X;

      let q be FinSequence of BOOLEAN ;

      

      thus ( len ( MergeSequence ( <*x*>,q))) = ( len <*x*>) by Def1

      .= 1 by FINSEQ_1: 39;

    end;

    theorem :: YELLOW15:10

    for X be set holds for x be Subset of X holds for q be FinSequence of BOOLEAN holds ((q . 1) = TRUE implies (( MergeSequence ( <*x*>,q)) . 1) = x) & ((q . 1) = FALSE implies (( MergeSequence ( <*x*>,q)) . 1) = (X \ x))

    proof

      let X be set;

      let x be Subset of X;

      let q be FinSequence of BOOLEAN ;

      thus (q . 1) = TRUE implies (( MergeSequence ( <*x*>,q)) . 1) = x

      proof

        assume (q . 1) = TRUE ;

        

        hence (( MergeSequence ( <*x*>,q)) . 1) = ( <*x*> . 1) by Th2

        .= x by FINSEQ_1: 40;

      end;

      1 in ( Seg 1) by FINSEQ_1: 1;

      then

       A1: 1 in ( dom <*x*>) by FINSEQ_1: 38;

      assume (q . 1) = FALSE ;

      

      hence (( MergeSequence ( <*x*>,q)) . 1) = (X \ ( <*x*> . 1)) by A1, Th3

      .= (X \ x) by FINSEQ_1: 40;

    end;

    theorem :: YELLOW15:11

    for X be set holds for x,y be Subset of X holds for q be FinSequence of BOOLEAN holds ( len ( MergeSequence ( <*x, y*>,q))) = 2

    proof

      let X be set;

      let x,y be Subset of X;

      let q be FinSequence of BOOLEAN ;

      

      thus ( len ( MergeSequence ( <*x, y*>,q))) = ( len <*x, y*>) by Def1

      .= 2 by FINSEQ_1: 44;

    end;

    theorem :: YELLOW15:12

    for X be set holds for x,y be Subset of X holds for q be FinSequence of BOOLEAN holds ((q . 1) = TRUE implies (( MergeSequence ( <*x, y*>,q)) . 1) = x) & ((q . 1) = FALSE implies (( MergeSequence ( <*x, y*>,q)) . 1) = (X \ x)) & ((q . 2) = TRUE implies (( MergeSequence ( <*x, y*>,q)) . 2) = y) & ((q . 2) = FALSE implies (( MergeSequence ( <*x, y*>,q)) . 2) = (X \ y))

    proof

      let X be set;

      let x,y be Subset of X;

      let q be FinSequence of BOOLEAN ;

      thus (q . 1) = TRUE implies (( MergeSequence ( <*x, y*>,q)) . 1) = x

      proof

        assume (q . 1) = TRUE ;

        

        hence (( MergeSequence ( <*x, y*>,q)) . 1) = ( <*x, y*> . 1) by Th2

        .= x by FINSEQ_1: 44;

      end;

      2 in ( Seg 2) by FINSEQ_1: 1;

      then

       A1: 2 in ( dom <*x, y*>) by FINSEQ_1: 89;

      1 in ( Seg 2) by FINSEQ_1: 1;

      then

       A2: 1 in ( dom <*x, y*>) by FINSEQ_1: 89;

      thus (q . 1) = FALSE implies (( MergeSequence ( <*x, y*>,q)) . 1) = (X \ x)

      proof

        assume (q . 1) = FALSE ;

        

        hence (( MergeSequence ( <*x, y*>,q)) . 1) = (X \ ( <*x, y*> . 1)) by A2, Th3

        .= (X \ x) by FINSEQ_1: 44;

      end;

      thus (q . 2) = TRUE implies (( MergeSequence ( <*x, y*>,q)) . 2) = y

      proof

        assume (q . 2) = TRUE ;

        

        hence (( MergeSequence ( <*x, y*>,q)) . 2) = ( <*x, y*> . 2) by Th2

        .= y by FINSEQ_1: 44;

      end;

      assume (q . 2) = FALSE ;

      

      hence (( MergeSequence ( <*x, y*>,q)) . 2) = (X \ ( <*x, y*> . 2)) by A1, Th3

      .= (X \ y) by FINSEQ_1: 44;

    end;

    theorem :: YELLOW15:13

    for X be set holds for x,y,z be Subset of X holds for q be FinSequence of BOOLEAN holds ( len ( MergeSequence ( <*x, y, z*>,q))) = 3

    proof

      let X be set;

      let x,y,z be Subset of X;

      let q be FinSequence of BOOLEAN ;

      

      thus ( len ( MergeSequence ( <*x, y, z*>,q))) = ( len <*x, y, z*>) by Def1

      .= 3 by FINSEQ_1: 45;

    end;

    theorem :: YELLOW15:14

    for X be set holds for x,y,z be Subset of X holds for q be FinSequence of BOOLEAN holds ((q . 1) = TRUE implies (( MergeSequence ( <*x, y, z*>,q)) . 1) = x) & ((q . 1) = FALSE implies (( MergeSequence ( <*x, y, z*>,q)) . 1) = (X \ x)) & ((q . 2) = TRUE implies (( MergeSequence ( <*x, y, z*>,q)) . 2) = y) & ((q . 2) = FALSE implies (( MergeSequence ( <*x, y, z*>,q)) . 2) = (X \ y)) & ((q . 3) = TRUE implies (( MergeSequence ( <*x, y, z*>,q)) . 3) = z) & ((q . 3) = FALSE implies (( MergeSequence ( <*x, y, z*>,q)) . 3) = (X \ z))

    proof

      let X be set;

      let x,y,z be Subset of X;

      let q be FinSequence of BOOLEAN ;

      thus (q . 1) = TRUE implies (( MergeSequence ( <*x, y, z*>,q)) . 1) = x

      proof

        assume (q . 1) = TRUE ;

        

        hence (( MergeSequence ( <*x, y, z*>,q)) . 1) = ( <*x, y, z*> . 1) by Th2

        .= x by FINSEQ_1: 45;

      end;

      3 in ( Seg 3) by FINSEQ_1: 1;

      then

       A1: 3 in ( dom <*x, y, z*>) by FINSEQ_1: 89;

      1 in ( Seg 3) by FINSEQ_1: 1;

      then

       A2: 1 in ( dom <*x, y, z*>) by FINSEQ_1: 89;

      thus (q . 1) = FALSE implies (( MergeSequence ( <*x, y, z*>,q)) . 1) = (X \ x)

      proof

        assume (q . 1) = FALSE ;

        

        hence (( MergeSequence ( <*x, y, z*>,q)) . 1) = (X \ ( <*x, y, z*> . 1)) by A2, Th3

        .= (X \ x) by FINSEQ_1: 45;

      end;

      thus (q . 2) = TRUE implies (( MergeSequence ( <*x, y, z*>,q)) . 2) = y

      proof

        assume (q . 2) = TRUE ;

        

        hence (( MergeSequence ( <*x, y, z*>,q)) . 2) = ( <*x, y, z*> . 2) by Th2

        .= y by FINSEQ_1: 45;

      end;

      2 in ( Seg 3) by FINSEQ_1: 1;

      then

       A3: 2 in ( dom <*x, y, z*>) by FINSEQ_1: 89;

      thus (q . 2) = FALSE implies (( MergeSequence ( <*x, y, z*>,q)) . 2) = (X \ y)

      proof

        assume (q . 2) = FALSE ;

        

        hence (( MergeSequence ( <*x, y, z*>,q)) . 2) = (X \ ( <*x, y, z*> . 2)) by A3, Th3

        .= (X \ y) by FINSEQ_1: 45;

      end;

      thus (q . 3) = TRUE implies (( MergeSequence ( <*x, y, z*>,q)) . 3) = z

      proof

        assume (q . 3) = TRUE ;

        

        hence (( MergeSequence ( <*x, y, z*>,q)) . 3) = ( <*x, y, z*> . 3) by Th2

        .= z by FINSEQ_1: 45;

      end;

      assume (q . 3) = FALSE ;

      

      hence (( MergeSequence ( <*x, y, z*>,q)) . 3) = (X \ ( <*x, y, z*> . 3)) by A1, Th3

      .= (X \ z) by FINSEQ_1: 45;

    end;

    theorem :: YELLOW15:15

    

     Th12: for X be set holds for p be FinSequence of ( bool X) holds { ( Intersect ( rng ( MergeSequence (p,q)))) where q be FinSequence of BOOLEAN : ( len q) = ( len p) } is Subset-Family of X

    proof

      let X be set;

      let p be FinSequence of ( bool X);

      { ( Intersect ( rng ( MergeSequence (p,q)))) where q be FinSequence of BOOLEAN : ( len q) = ( len p) } c= ( bool X)

      proof

        let z be object;

        assume z in { ( Intersect ( rng ( MergeSequence (p,q)))) where q be FinSequence of BOOLEAN : ( len q) = ( len p) };

        then ex q be FinSequence of BOOLEAN st z = ( Intersect ( rng ( MergeSequence (p,q)))) & ( len q) = ( len p);

        hence thesis;

      end;

      hence thesis;

    end;

    registration

      cluster -> boolean-valued for FinSequence of BOOLEAN ;

      coherence

      proof

        let f be FinSequence of BOOLEAN ;

        thus ( rng f) c= BOOLEAN ;

      end;

    end

    definition

      let X be set;

      let Y be finite Subset-Family of X;

      :: YELLOW15:def2

      func Components (Y) -> Subset-Family of X means

      : Def2: ex p be FinSequence of ( bool X) st ( len p) = ( card Y) & ( rng p) = Y & it = { ( Intersect ( rng ( MergeSequence (p,q)))) where q be FinSequence of BOOLEAN : ( len q) = ( len p) };

      existence

      proof

        consider p be FinSequence such that

         A1: ( rng p) = Y and

         A2: p is one-to-one by FINSEQ_4: 58;

        reconsider p as FinSequence of ( bool X) by A1, FINSEQ_1:def 4;

        reconsider C = { ( Intersect ( rng ( MergeSequence (p,q)))) where q be FinSequence of BOOLEAN : ( len q) = ( len p) } as Subset-Family of X by Th12;

        take C, p;

        thus thesis by A1, A2, FINSEQ_4: 62;

      end;

      uniqueness

      proof

        let C1,C2 be Subset-Family of X such that

         A3: ex p be FinSequence of ( bool X) st ( len p) = ( card Y) & ( rng p) = Y & C1 = { ( Intersect ( rng ( MergeSequence (p,q)))) where q be FinSequence of BOOLEAN : ( len q) = ( len p) } and

         A4: ex p be FinSequence of ( bool X) st ( len p) = ( card Y) & ( rng p) = Y & C2 = { ( Intersect ( rng ( MergeSequence (p,q)))) where q be FinSequence of BOOLEAN : ( len q) = ( len p) };

        consider p1 be FinSequence of ( bool X) such that

         A5: ( len p1) = ( card Y) and

         A6: ( rng p1) = Y and

         A7: C1 = { ( Intersect ( rng ( MergeSequence (p1,q)))) where q be FinSequence of BOOLEAN : ( len q) = ( len p1) } by A3;

        consider p2 be FinSequence of ( bool X) such that

         A8: ( len p2) = ( card Y) and

         A9: ( rng p2) = Y and

         A10: C2 = { ( Intersect ( rng ( MergeSequence (p2,q)))) where q be FinSequence of BOOLEAN : ( len q) = ( len p2) } by A4;

        

         A11: p2 is one-to-one by A8, A9, FINSEQ_4: 62;

        

         A12: p1 is one-to-one by A5, A6, FINSEQ_4: 62;

        now

          let P be Subset of X;

          thus P in C1 implies P in C2

          proof

            p1 is Function of ( dom p1), ( rng p1) by FUNCT_2: 1;

            then

             A13: (p1 " ) is Function of ( rng p1), ( dom p1) by A12, FUNCT_2: 25;

            p2 is FinSequence of ( rng p1) by A6, A9, FINSEQ_1:def 4;

            then

             A14: ((p1 " ) * p2) is FinSequence of ( dom p1) by A13, FINSEQ_2: 32;

            assume P in C1;

            then

            consider q be FinSequence of BOOLEAN such that

             A15: P = ( Intersect ( rng ( MergeSequence (p1,q)))) and

             A16: ( len q) = ( len p1) by A7;

            

             A17: ( dom p1) = ( Seg ( len q)) by A16, FINSEQ_1:def 3

            .= ( dom q) by FINSEQ_1:def 3;

            then q is Function of ( dom p1), BOOLEAN by FINSEQ_2: 26;

            then (q * ((p1 " ) * p2)) is FinSequence of BOOLEAN by A14, FINSEQ_2: 32;

            then

            reconsider q1 = ((q * (p1 " )) * p2) as FinSequence of BOOLEAN by RELAT_1: 36;

            

             A18: ( rng p2) = ( dom (p1 " )) by A6, A9, A12, FUNCT_1: 33;

            then

             A19: ( dom ((p1 " ) * p2)) = ( dom p2) by RELAT_1: 27;

            ( rng ((p1 " ) * p2)) = ( rng (p1 " )) by A18, RELAT_1: 28

            .= ( dom q) by A12, A17, FUNCT_1: 33;

            then

             A20: ( dom (q * ((p1 " ) * p2))) = ( dom p2) by A19, RELAT_1: 27;

            

             A21: ( rng p1) = ( dom (p2 " )) by A6, A9, A11, FUNCT_1: 33;

            then

             A22: ( dom ((p2 " ) * p1)) = ( dom p1) by RELAT_1: 27;

            

             A23: ( Seg ( len q1)) = ( dom q1) by FINSEQ_1:def 3

            .= ( dom p2) by A20, RELAT_1: 36

            .= ( Seg ( len p2)) by FINSEQ_1:def 3;

            

            then

             A24: ( dom p2) = ( Seg ( len q1)) by FINSEQ_1:def 3

            .= ( dom q1) by FINSEQ_1:def 3;

            ( rng ((p2 " ) * p1)) = ( rng (p2 " )) by A21, RELAT_1: 28

            .= ( dom q1) by A11, A24, FUNCT_1: 33;

            then

             A25: ( dom (q1 * ((p2 " ) * p1))) = ( dom p1) by A22, RELAT_1: 27;

            

             A26: ((q1 * (p2 " )) * p1) = (((q * (p1 " )) * p2) * ((p2 " ) * p1)) by RELAT_1: 36

            .= ((q * (p1 " )) * (p2 * ((p2 " ) * p1))) by RELAT_1: 36

            .= ((q * (p1 " )) * ((p2 * (p2 " )) * p1)) by RELAT_1: 36

            .= ((q * (p1 " )) * (( id ( rng p2)) * p1)) by A11, FUNCT_1: 39

            .= ((q * (p1 " )) * p1) by A6, A9, RELAT_1: 54

            .= (q * ((p1 " ) * p1)) by RELAT_1: 36

            .= (q * ( id ( dom p1))) by A12, FUNCT_1: 39

            .= q by A17, RELAT_1: 52;

            

             A27: ( rng ( MergeSequence (p1,q))) c= ( rng ( MergeSequence (p2,q1)))

            proof

              let z be object;

              assume z in ( rng ( MergeSequence (p1,q)));

              then

              consider j be Nat such that

               A28: j in ( dom ( MergeSequence (p1,q))) and

               A29: (( MergeSequence (p1,q)) . j) = z by FINSEQ_2: 10;

              j in ( Seg ( len ( MergeSequence (p1,q)))) by A28, FINSEQ_1:def 3;

              then

               A30: j in ( Seg ( len p1)) by Def1;

              then

               A31: j in ( dom (q1 * ((p2 " ) * p1))) by A25, FINSEQ_1:def 3;

              

               A32: j in ( dom p1) by A30, FINSEQ_1:def 3;

              then

               A33: j in ( dom ((p2 " ) * p1)) by A21, RELAT_1: 27;

              then (((p2 " ) * p1) . j) in ( rng ((p2 " ) * p1)) by FUNCT_1:def 3;

              then (((p2 " ) * p1) . j) in ( rng (p2 " )) by FUNCT_1: 14;

              then

               A34: (((p2 " ) * p1) . j) in ( dom p2) by A11, FUNCT_1: 33;

              then

              reconsider pj = (((p2 " ) * p1) . j) as Element of NAT ;

              

               A35: (q . j) = ((q1 * ((p2 " ) * p1)) . j) by A26, RELAT_1: 36

              .= (q1 . (((p2 " ) * p1) . j)) by A31, FUNCT_1: 12;

               A36:

              now

                per cases by XBOOLEAN:def 3;

                  suppose

                   A37: (q . j) = TRUE ;

                  

                  hence (( MergeSequence (p2,q1)) . (((p2 " ) * p1) . j)) = (p2 . pj) by A35, Th2

                  .= ((p2 * ((p2 " ) * p1)) . j) by A33, FUNCT_1: 13

                  .= (((p2 * (p2 " )) * p1) . j) by RELAT_1: 36

                  .= ((( id ( rng p1)) * p1) . j) by A6, A9, A11, FUNCT_1: 39

                  .= (p1 . j) by RELAT_1: 54

                  .= z by A29, A37, Th2;

                end;

                  suppose

                   A38: (q . j) = FALSE ;

                  

                  hence (( MergeSequence (p2,q1)) . (((p2 " ) * p1) . j)) = (X \ (p2 . pj)) by A34, A35, Th3

                  .= (X \ ((p2 * ((p2 " ) * p1)) . j)) by A33, FUNCT_1: 13

                  .= (X \ (((p2 * (p2 " )) * p1) . j)) by RELAT_1: 36

                  .= (X \ ((( id ( rng p1)) * p1) . j)) by A6, A9, A11, FUNCT_1: 39

                  .= (X \ (p1 . j)) by RELAT_1: 54

                  .= z by A29, A32, Th3, A38;

                end;

              end;

              (((p2 " ) * p1) . j) in ( Seg ( len p2)) by A34, FINSEQ_1:def 3;

              then (((p2 " ) * p1) . j) in ( Seg ( len ( MergeSequence (p2,q1)))) by Def1;

              then (((p2 " ) * p1) . j) in ( dom ( MergeSequence (p2,q1))) by FINSEQ_1:def 3;

              hence thesis by A36, FUNCT_1:def 3;

            end;

            

             A39: ( len q1) = ( len p2) by A23, FINSEQ_1: 6;

            ( rng ( MergeSequence (p2,q1))) c= ( rng ( MergeSequence (p1,q)))

            proof

              let z be object;

              assume z in ( rng ( MergeSequence (p2,q1)));

              then

              consider j be Nat such that

               A40: j in ( dom ( MergeSequence (p2,q1))) and

               A41: (( MergeSequence (p2,q1)) . j) = z by FINSEQ_2: 10;

              j in ( Seg ( len ( MergeSequence (p2,q1)))) by A40, FINSEQ_1:def 3;

              then

               A42: j in ( Seg ( len p2)) by Def1;

              then

               A43: j in ( dom (q * ((p1 " ) * p2))) by A20, FINSEQ_1:def 3;

              

               A44: j in ( dom p2) by A42, FINSEQ_1:def 3;

              then

               A45: j in ( dom ((p1 " ) * p2)) by A18, RELAT_1: 27;

              then (((p1 " ) * p2) . j) in ( rng ((p1 " ) * p2)) by FUNCT_1:def 3;

              then (((p1 " ) * p2) . j) in ( rng (p1 " )) by FUNCT_1: 14;

              then

               A46: (((p1 " ) * p2) . j) in ( dom p1) by A12, FUNCT_1: 33;

              then

              reconsider pj = (((p1 " ) * p2) . j) as Element of NAT ;

              

               A47: (q1 . j) = ((q * ((p1 " ) * p2)) . j) by RELAT_1: 36

              .= (q . (((p1 " ) * p2) . j)) by A43, FUNCT_1: 12;

               A48:

              now

                per cases by XBOOLEAN:def 3;

                  suppose

                   A49: (q1 . j) = TRUE ;

                  

                  hence (( MergeSequence (p1,q)) . (((p1 " ) * p2) . j)) = (p1 . pj) by A47, Th2

                  .= ((p1 * ((p1 " ) * p2)) . j) by A45, FUNCT_1: 13

                  .= (((p1 * (p1 " )) * p2) . j) by RELAT_1: 36

                  .= ((( id ( rng p2)) * p2) . j) by A6, A9, A12, FUNCT_1: 39

                  .= (p2 . j) by RELAT_1: 54

                  .= z by A41, A49, Th2;

                end;

                  suppose

                   A50: (q1 . j) = FALSE ;

                  

                  hence (( MergeSequence (p1,q)) . (((p1 " ) * p2) . j)) = (X \ (p1 . pj)) by A46, A47, Th3

                  .= (X \ ((p1 * ((p1 " ) * p2)) . j)) by A45, FUNCT_1: 13

                  .= (X \ (((p1 * (p1 " )) * p2) . j)) by RELAT_1: 36

                  .= (X \ ((( id ( rng p2)) * p2) . j)) by A6, A9, A12, FUNCT_1: 39

                  .= (X \ (p2 . j)) by RELAT_1: 54

                  .= z by A41, A44, A50, Th3;

                end;

              end;

              (((p1 " ) * p2) . j) in ( Seg ( len p1)) by A46, FINSEQ_1:def 3;

              then (((p1 " ) * p2) . j) in ( Seg ( len ( MergeSequence (p1,q)))) by Def1;

              then (((p1 " ) * p2) . j) in ( dom ( MergeSequence (p1,q))) by FINSEQ_1:def 3;

              hence thesis by A48, FUNCT_1:def 3;

            end;

            then P = ( Intersect ( rng ( MergeSequence (p2,q1)))) by A15, A27, XBOOLE_0:def 10;

            hence thesis by A10, A39;

          end;

          thus P in C2 implies P in C1

          proof

            p2 is Function of ( dom p2), ( rng p2) by FUNCT_2: 1;

            then

             A51: (p2 " ) is Function of ( rng p2), ( dom p2) by A11, FUNCT_2: 25;

            p1 is FinSequence of ( rng p2) by A6, A9, FINSEQ_1:def 4;

            then

             A52: ((p2 " ) * p1) is FinSequence of ( dom p2) by A51, FINSEQ_2: 32;

            assume P in C2;

            then

            consider q be FinSequence of BOOLEAN such that

             A53: P = ( Intersect ( rng ( MergeSequence (p2,q)))) and

             A54: ( len q) = ( len p2) by A10;

            

             A55: ( dom p2) = ( Seg ( len q)) by A54, FINSEQ_1:def 3

            .= ( dom q) by FINSEQ_1:def 3;

            then q is Function of ( dom p2), BOOLEAN by FINSEQ_2: 26;

            then (q * ((p2 " ) * p1)) is FinSequence of BOOLEAN by A52, FINSEQ_2: 32;

            then

            reconsider q1 = ((q * (p2 " )) * p1) as FinSequence of BOOLEAN by RELAT_1: 36;

            

             A56: ( rng p1) = ( dom (p2 " )) by A6, A9, A11, FUNCT_1: 33;

            then

             A57: ( dom ((p2 " ) * p1)) = ( dom p1) by RELAT_1: 27;

            ( rng ((p2 " ) * p1)) = ( rng (p2 " )) by A56, RELAT_1: 28

            .= ( dom q) by A11, A55, FUNCT_1: 33;

            then

             A58: ( dom (q * ((p2 " ) * p1))) = ( dom p1) by A57, RELAT_1: 27;

            

             A59: ( rng p2) = ( dom (p1 " )) by A6, A9, A12, FUNCT_1: 33;

            then

             A60: ( dom ((p1 " ) * p2)) = ( dom p2) by RELAT_1: 27;

            

             A61: ( Seg ( len q1)) = ( dom q1) by FINSEQ_1:def 3

            .= ( dom p1) by A58, RELAT_1: 36

            .= ( Seg ( len p1)) by FINSEQ_1:def 3;

            

            then

             A62: ( dom p1) = ( Seg ( len q1)) by FINSEQ_1:def 3

            .= ( dom q1) by FINSEQ_1:def 3;

            ( rng ((p1 " ) * p2)) = ( rng (p1 " )) by A59, RELAT_1: 28

            .= ( dom q1) by A12, A62, FUNCT_1: 33;

            then

             A63: ( dom (q1 * ((p1 " ) * p2))) = ( dom p2) by A60, RELAT_1: 27;

            

             A64: ((q1 * (p1 " )) * p2) = (((q * (p2 " )) * p1) * ((p1 " ) * p2)) by RELAT_1: 36

            .= ((q * (p2 " )) * (p1 * ((p1 " ) * p2))) by RELAT_1: 36

            .= ((q * (p2 " )) * ((p1 * (p1 " )) * p2)) by RELAT_1: 36

            .= ((q * (p2 " )) * (( id ( rng p1)) * p2)) by A12, FUNCT_1: 39

            .= ((q * (p2 " )) * p2) by A6, A9, RELAT_1: 54

            .= (q * ((p2 " ) * p2)) by RELAT_1: 36

            .= (q * ( id ( dom p2))) by A11, FUNCT_1: 39

            .= q by A55, RELAT_1: 52;

            

             A65: ( rng ( MergeSequence (p2,q))) c= ( rng ( MergeSequence (p1,q1)))

            proof

              let z be object;

              assume z in ( rng ( MergeSequence (p2,q)));

              then

              consider j be Nat such that

               A66: j in ( dom ( MergeSequence (p2,q))) and

               A67: (( MergeSequence (p2,q)) . j) = z by FINSEQ_2: 10;

              j in ( Seg ( len ( MergeSequence (p2,q)))) by A66, FINSEQ_1:def 3;

              then

               A68: j in ( Seg ( len p2)) by Def1;

              then

               A69: j in ( dom (q1 * ((p1 " ) * p2))) by A63, FINSEQ_1:def 3;

              

               A70: j in ( dom p2) by A68, FINSEQ_1:def 3;

              then

               A71: j in ( dom ((p1 " ) * p2)) by A59, RELAT_1: 27;

              then (((p1 " ) * p2) . j) in ( rng ((p1 " ) * p2)) by FUNCT_1:def 3;

              then (((p1 " ) * p2) . j) in ( rng (p1 " )) by FUNCT_1: 14;

              then

               A72: (((p1 " ) * p2) . j) in ( dom p1) by A12, FUNCT_1: 33;

              then

              reconsider pj = (((p1 " ) * p2) . j) as Element of NAT ;

              

               A73: (q . j) = ((q1 * ((p1 " ) * p2)) . j) by A64, RELAT_1: 36

              .= (q1 . (((p1 " ) * p2) . j)) by A69, FUNCT_1: 12;

               A74:

              now

                per cases by XBOOLEAN:def 3;

                  suppose

                   A75: (q . j) = TRUE ;

                  

                  hence (( MergeSequence (p1,q1)) . (((p1 " ) * p2) . j)) = (p1 . pj) by A73, Th2

                  .= ((p1 * ((p1 " ) * p2)) . j) by A71, FUNCT_1: 13

                  .= (((p1 * (p1 " )) * p2) . j) by RELAT_1: 36

                  .= ((( id ( rng p2)) * p2) . j) by A6, A9, A12, FUNCT_1: 39

                  .= (p2 . j) by RELAT_1: 54

                  .= z by A67, A75, Th2;

                end;

                  suppose

                   A76: (q . j) = FALSE ;

                  

                  hence (( MergeSequence (p1,q1)) . (((p1 " ) * p2) . j)) = (X \ (p1 . pj)) by A72, A73, Th3

                  .= (X \ ((p1 * ((p1 " ) * p2)) . j)) by A71, FUNCT_1: 13

                  .= (X \ (((p1 * (p1 " )) * p2) . j)) by RELAT_1: 36

                  .= (X \ ((( id ( rng p2)) * p2) . j)) by A6, A9, A12, FUNCT_1: 39

                  .= (X \ (p2 . j)) by RELAT_1: 54

                  .= z by A67, A70, A76, Th3;

                end;

              end;

              (((p1 " ) * p2) . j) in ( Seg ( len p1)) by A72, FINSEQ_1:def 3;

              then (((p1 " ) * p2) . j) in ( Seg ( len ( MergeSequence (p1,q1)))) by Def1;

              then (((p1 " ) * p2) . j) in ( dom ( MergeSequence (p1,q1))) by FINSEQ_1:def 3;

              hence thesis by A74, FUNCT_1:def 3;

            end;

            

             A77: ( len q1) = ( len p1) by A61, FINSEQ_1: 6;

            ( rng ( MergeSequence (p1,q1))) c= ( rng ( MergeSequence (p2,q)))

            proof

              let z be object;

              assume z in ( rng ( MergeSequence (p1,q1)));

              then

              consider j be Nat such that

               A78: j in ( dom ( MergeSequence (p1,q1))) and

               A79: (( MergeSequence (p1,q1)) . j) = z by FINSEQ_2: 10;

              j in ( Seg ( len ( MergeSequence (p1,q1)))) by A78, FINSEQ_1:def 3;

              then

               A80: j in ( Seg ( len p1)) by Def1;

              then

               A81: j in ( dom (q * ((p2 " ) * p1))) by A58, FINSEQ_1:def 3;

              

               A82: j in ( dom p1) by A80, FINSEQ_1:def 3;

              then

               A83: j in ( dom ((p2 " ) * p1)) by A56, RELAT_1: 27;

              then (((p2 " ) * p1) . j) in ( rng ((p2 " ) * p1)) by FUNCT_1:def 3;

              then (((p2 " ) * p1) . j) in ( rng (p2 " )) by FUNCT_1: 14;

              then

               A84: (((p2 " ) * p1) . j) in ( dom p2) by A11, FUNCT_1: 33;

              then

              reconsider pj = (((p2 " ) * p1) . j) as Element of NAT ;

              

               A85: (q1 . j) = ((q * ((p2 " ) * p1)) . j) by RELAT_1: 36

              .= (q . (((p2 " ) * p1) . j)) by A81, FUNCT_1: 12;

               A86:

              now

                per cases by XBOOLEAN:def 3;

                  suppose

                   A87: (q1 . j) = TRUE ;

                  

                  hence (( MergeSequence (p2,q)) . (((p2 " ) * p1) . j)) = (p2 . pj) by A85, Th2

                  .= ((p2 * ((p2 " ) * p1)) . j) by A83, FUNCT_1: 13

                  .= (((p2 * (p2 " )) * p1) . j) by RELAT_1: 36

                  .= ((( id ( rng p1)) * p1) . j) by A6, A9, A11, FUNCT_1: 39

                  .= (p1 . j) by RELAT_1: 54

                  .= z by A79, A87, Th2;

                end;

                  suppose

                   A88: (q1 . j) = FALSE ;

                  

                  hence (( MergeSequence (p2,q)) . (((p2 " ) * p1) . j)) = (X \ (p2 . pj)) by A84, A85, Th3

                  .= (X \ ((p2 * ((p2 " ) * p1)) . j)) by A83, FUNCT_1: 13

                  .= (X \ (((p2 * (p2 " )) * p1) . j)) by RELAT_1: 36

                  .= (X \ ((( id ( rng p1)) * p1) . j)) by A6, A9, A11, FUNCT_1: 39

                  .= (X \ (p1 . j)) by RELAT_1: 54

                  .= z by A79, A82, A88, Th3;

                end;

              end;

              (((p2 " ) * p1) . j) in ( Seg ( len p2)) by A84, FINSEQ_1:def 3;

              then (((p2 " ) * p1) . j) in ( Seg ( len ( MergeSequence (p2,q)))) by Def1;

              then (((p2 " ) * p1) . j) in ( dom ( MergeSequence (p2,q))) by FINSEQ_1:def 3;

              hence thesis by A86, FUNCT_1:def 3;

            end;

            then P = ( Intersect ( rng ( MergeSequence (p1,q1)))) by A53, A65, XBOOLE_0:def 10;

            hence thesis by A7, A77;

          end;

        end;

        hence thesis by SETFAM_1: 31;

      end;

    end

    registration

      let X be set;

      let Y be finite Subset-Family of X;

      cluster ( Components Y) -> finite;

      coherence

      proof

        consider p be FinSequence of ( bool X) such that ( len p) = ( card Y) and ( rng p) = Y and

         A1: ( Components Y) = { ( Intersect ( rng ( MergeSequence (p,q)))) where q be FinSequence of BOOLEAN : ( len q) = ( len p) } by Def2;

        deffunc F( Element of ( BOOLEAN * )) = ( Intersect ( rng ( MergeSequence (p,$1))));

        

         A2: ( Components Y) c= { ( Intersect ( rng ( MergeSequence (p,q)))) where q be Element of ( BOOLEAN * ) : q in (( len p) -tuples_on BOOLEAN ) }

        proof

          let z be object;

          assume z in ( Components Y);

          then

          consider q be FinSequence of BOOLEAN such that

           A3: z = ( Intersect ( rng ( MergeSequence (p,q)))) & ( len q) = ( len p) by A1;

          q is Element of ( BOOLEAN * ) & q is Element of (( len q) -tuples_on BOOLEAN ) by FINSEQ_1:def 11, FINSEQ_2: 92;

          hence thesis by A3;

        end;

        

         A4: (( len p) -tuples_on BOOLEAN ) is finite;

        { F(q) where q be Element of ( BOOLEAN * ) : q in (( len p) -tuples_on BOOLEAN ) } is finite from FRAENKEL:sch 21( A4);

        hence thesis by A2;

      end;

    end

    theorem :: YELLOW15:16

    

     Th13: for X be set holds for Y be empty Subset-Family of X holds ( Components Y) = {X}

    proof

      let X be set;

      let Y be empty Subset-Family of X;

      consider p be FinSequence of ( bool X) such that

       A1: ( len p) = ( card Y) and

       A2: ( rng p) = Y and

       A3: ( Components Y) = { ( Intersect ( rng ( MergeSequence (p,q)))) where q be FinSequence of BOOLEAN : ( len q) = ( len p) } by Def2;

      thus ( Components Y) = {X}

      proof

        thus ( Components Y) c= {X}

        proof

          let z be object;

          assume z in ( Components Y);

          then

          consider q be FinSequence of BOOLEAN such that

           A4: z = ( Intersect ( rng ( MergeSequence (p,q)))) and ( len q) = ( len p) by A3;

          p = ( <*> ( bool X)) by A2;

          then ( rng ( MergeSequence (p,q))) = {} by Th5, RELAT_1: 38;

          then ( Intersect ( rng ( MergeSequence (p,q)))) = X by SETFAM_1:def 9;

          hence thesis by A4, TARSKI:def 1;

        end;

        let z be object;

        p = ( <*> ( bool X)) by A2;

        then ( rng ( MergeSequence (p,( <*> BOOLEAN )))) = {} by Th5, RELAT_1: 38;

        then

         A5: ( Intersect ( rng ( MergeSequence (p,( <*> BOOLEAN ))))) = X by SETFAM_1:def 9;

        assume z in {X};

        then z = X by TARSKI:def 1;

        hence thesis by A1, A3, A5;

      end;

    end;

    theorem :: YELLOW15:17

    for X be set holds for Y,Z be finite Subset-Family of X st Z c= Y holds ( Components Y) is_finer_than ( Components Z)

    proof

      let X be set;

      let Y,Z be finite Subset-Family of X;

      assume

       A1: Z c= Y;

      now

        let V be set;

        consider p be FinSequence of ( bool X) such that

         A2: ( len p) = ( card Y) and

         A3: ( rng p) = Y and

         A4: ( Components Y) = { ( Intersect ( rng ( MergeSequence (p,q)))) where q be FinSequence of BOOLEAN : ( len q) = ( len p) } by Def2;

        consider p1 be FinSequence of ( bool X) such that ( len p1) = ( card Z) and

         A5: ( rng p1) = Z and

         A6: ( Components Z) = { ( Intersect ( rng ( MergeSequence (p1,q)))) where q be FinSequence of BOOLEAN : ( len q) = ( len p1) } by Def2;

        

         A7: p1 is FinSequence of ( rng p) by A1, A3, A5, FINSEQ_1:def 4;

        assume V in ( Components Y);

        then

        consider q be FinSequence of BOOLEAN such that

         A8: V = ( Intersect ( rng ( MergeSequence (p,q)))) and

         A9: ( len q) = ( len p) by A4;

        ( dom p) = ( dom q) by A9, FINSEQ_3: 29;

        then

         A10: q is Function of ( dom p), BOOLEAN by FINSEQ_2: 26;

        

         A11: p is one-to-one by A2, A3, FINSEQ_4: 62;

        then

         A12: ( rng p1) c= ( dom (p " )) by A1, A3, A5, FUNCT_1: 33;

        ( rng (p " )) = ( dom p) by A11, FUNCT_1: 33

        .= ( dom q) by A9, FINSEQ_3: 29;

        then

         A13: ( rng ((p " ) * p1)) c= ( dom q) by RELAT_1: 26;

        p is Function of ( dom p), ( rng p) by FUNCT_2: 1;

        then (p " ) is Function of ( rng p), ( dom p) by A11, FUNCT_2: 25;

        then ((p " ) * p1) is FinSequence of ( dom p) by A7, FINSEQ_2: 32;

        then (q * ((p " ) * p1)) is FinSequence of BOOLEAN by A10, FINSEQ_2: 32;

        then

        reconsider q1 = ((q * (p " )) * p1) as FinSequence of BOOLEAN by RELAT_1: 36;

        reconsider W = ( Intersect ( rng ( MergeSequence (p1,q1)))) as set;

        take W;

        ( dom q1) = ( dom (q * ((p " ) * p1))) by RELAT_1: 36

        .= ( dom ((p " ) * p1)) by A13, RELAT_1: 27

        .= ( dom p1) by A12, RELAT_1: 27;

        then ( len q1) = ( len p1) by FINSEQ_3: 29;

        hence W in ( Components Z) by A6;

        ( rng ( MergeSequence (p1,q1))) c= ( rng ( MergeSequence (p,q)))

        proof

          let z be object;

          assume z in ( rng ( MergeSequence (p1,q1)));

          then

          consider i be Nat such that

           A14: i in ( dom ( MergeSequence (p1,q1))) and

           A15: (( MergeSequence (p1,q1)) . i) = z by FINSEQ_2: 10;

          

           A16: i in ( dom p1) by A14, Th1;

          then

           A17: i in ( dom ((p " ) * p1)) by A12, RELAT_1: 27;

          then (((p " ) * p1) . i) in ( rng ((p " ) * p1)) by FUNCT_1:def 3;

          then

           A18: (((p " ) * p1) . i) in ( rng (p " )) by FUNCT_1: 14;

          then

           A19: (((p " ) * p1) . i) in ( dom p) by A11, FUNCT_1: 33;

          then

          reconsider j = (((p " ) * p1) . i) as Element of NAT ;

          

           A20: (q . j) = ((q * ((p " ) * p1)) . i) by A17, FUNCT_1: 13

          .= (q1 . i) by RELAT_1: 36;

          

           A21: p1 is Function of ( dom p1), ( rng p) by A1, A3, A5, FUNCT_2: 2;

          

           A22: j in ( dom p) by A11, A18, FUNCT_1: 33;

           A23:

          now

            per cases by XBOOLEAN:def 3;

              suppose

               A24: (q . j) = TRUE ;

              

              hence (( MergeSequence (p,q)) . j) = (p . j) by Th2

              .= ((p * ((p " ) * p1)) . i) by A17, FUNCT_1: 13

              .= (((p * (p " )) * p1) . i) by RELAT_1: 36

              .= ((( id ( rng p)) * p1) . i) by A11, FUNCT_1: 39

              .= (p1 . i) by A21, FUNCT_2: 17

              .= z by A15, A20, A24, Th2;

            end;

              suppose

               A25: (q . j) = FALSE ;

              

              hence (( MergeSequence (p,q)) . j) = (X \ (p . j)) by A22, Th3

              .= (X \ ((p * ((p " ) * p1)) . i)) by A17, FUNCT_1: 13

              .= (X \ (((p * (p " )) * p1) . i)) by RELAT_1: 36

              .= (X \ ((( id ( rng p)) * p1) . i)) by A11, FUNCT_1: 39

              .= (X \ (p1 . i)) by A21, FUNCT_2: 17

              .= z by A15, A16, A20, A25, Th3;

            end;

          end;

          j in ( dom ( MergeSequence (p,q))) by A19, Th1;

          hence thesis by A23, FUNCT_1:def 3;

        end;

        hence V c= W by A8, SETFAM_1: 44;

      end;

      hence thesis by SETFAM_1:def 2;

    end;

    theorem :: YELLOW15:18

    

     Th15: for X be set holds for Y be finite Subset-Family of X holds ( union ( Components Y)) = X

    proof

      let X be set;

      let Y be finite Subset-Family of X;

      X c= ( union ( Components Y))

      proof

        deffunc F( set) = FALSE ;

        deffunc T( set) = TRUE ;

        let z be object;

        consider p be FinSequence of ( bool X) such that ( len p) = ( card Y) and ( rng p) = Y and

         A1: ( Components Y) = { ( Intersect ( rng ( MergeSequence (p,q)))) where q be FinSequence of BOOLEAN : ( len q) = ( len p) } by Def2;

        defpred C[ set] means z in (p . $1);

        

         A2: for i be Nat st i in ( Seg ( len p)) holds ( C[i] implies T(i) in BOOLEAN ) & ( not C[i] implies F(i) in BOOLEAN );

        consider q be FinSequence of BOOLEAN such that

         A3: ( len q) = ( len p) and

         A4: for i be Nat st i in ( Seg ( len p)) holds ( C[i] implies (q . i) = T(i)) & ( not C[i] implies (q . i) = F(i)) from SeqLambda1C( A2);

        assume

         A5: z in X;

        now

          let Z be set;

          assume Z in ( rng ( MergeSequence (p,q)));

          then

          consider i be Nat such that

           A6: i in ( dom ( MergeSequence (p,q))) and

           A7: (( MergeSequence (p,q)) . i) = Z by FINSEQ_2: 10;

          

           A8: ( dom ( MergeSequence (p,q))) = ( dom p) by Th1;

          then

           A9: ( dom ( MergeSequence (p,q))) = ( Seg ( len p)) by FINSEQ_1:def 3;

          now

            per cases ;

              suppose

               A10: z in (p . i);

              then (q . i) = TRUE by A4, A6, A9;

              hence z in Z by A7, A10, Th2;

            end;

              suppose

               A11: not z in (p . i);

              then (q . i) = FALSE by A4, A6, A9;

              then (( MergeSequence (p,q)) . i) = (X \ (p . i)) by A6, A8, Th3;

              hence z in Z by A5, A7, A11, XBOOLE_0:def 5;

            end;

          end;

          hence z in Z;

        end;

        then

         A12: z in ( Intersect ( rng ( MergeSequence (p,q)))) by A5, SETFAM_1: 43;

        ( Intersect ( rng ( MergeSequence (p,q)))) in ( Components Y) by A1, A3;

        hence thesis by A12, TARSKI:def 4;

      end;

      hence thesis;

    end;

    theorem :: YELLOW15:19

    

     Th16: for X be set holds for Y be finite Subset-Family of X holds for A,B be set st A in ( Components Y) & B in ( Components Y) & A <> B holds A misses B

    proof

      let X be set;

      let Y be finite Subset-Family of X;

      let A,B be set;

      assume that

       A1: A in ( Components Y) and

       A2: B in ( Components Y) and

       A3: A <> B;

      assume (A /\ B) <> {} ;

      then

      consider z be object such that

       A4: z in (A /\ B) by XBOOLE_0:def 1;

      

       A5: z in B by A4, XBOOLE_0:def 4;

      

       A6: z in A by A4, XBOOLE_0:def 4;

      consider p be FinSequence of ( bool X) such that ( len p) = ( card Y) and ( rng p) = Y and

       A7: ( Components Y) = { ( Intersect ( rng ( MergeSequence (p,q)))) where q be FinSequence of BOOLEAN : ( len q) = ( len p) } by Def2;

      consider q1 be FinSequence of BOOLEAN such that

       A8: A = ( Intersect ( rng ( MergeSequence (p,q1)))) and ( len q1) = ( len p) by A1, A7;

      consider q2 be FinSequence of BOOLEAN such that

       A9: B = ( Intersect ( rng ( MergeSequence (p,q2)))) and ( len q2) = ( len p) by A2, A7;

      

       A10: ( len ( MergeSequence (p,q1))) = ( len p) by Def1;

      then

       A11: ( dom ( MergeSequence (p,q1))) = ( Seg ( len p)) by FINSEQ_1:def 3;

       A12:

      now

        let i be Nat;

        assume

         A13: i in ( dom ( MergeSequence (p,q1)));

        then

         A14: i in ( dom p) by A11, FINSEQ_1:def 3;

        (( MergeSequence (p,q1)) . i) in ( rng ( MergeSequence (p,q1))) by A13, FUNCT_1:def 3;

        then

         A15: z in (( MergeSequence (p,q1)) . i) by A8, A6, SETFAM_1: 43;

        i in ( dom ( MergeSequence (p,q2))) by A14, Th1;

        then (( MergeSequence (p,q2)) . i) in ( rng ( MergeSequence (p,q2))) by FUNCT_1:def 3;

        then

         A16: z in (( MergeSequence (p,q2)) . i) by A9, A5, SETFAM_1: 43;

        per cases by XBOOLEAN:def 3;

          suppose (q1 . i) = TRUE ;

          then

           A17: (( MergeSequence (p,q1)) . i) = (p . i) by Th2;

          (q2 . i) = TRUE

          proof

            assume not (q2 . i) = TRUE ;

            then (( MergeSequence (p,q2)) . i) = (X \ (p . i)) by A14, Th3, XBOOLEAN:def 3;

            hence contradiction by A15, A16, A17, XBOOLE_0:def 5;

          end;

          hence (( MergeSequence (p,q1)) . i) = (( MergeSequence (p,q2)) . i) by A17, Th2;

        end;

          suppose (q1 . i) = FALSE ;

          then

           A18: (( MergeSequence (p,q1)) . i) = (X \ (p . i)) by A14, Th3;

          (q2 . i) = FALSE

          proof

            assume not (q2 . i) = FALSE ;

            then (q2 . i) = TRUE by XBOOLEAN:def 3;

            then (( MergeSequence (p,q2)) . i) = (p . i) by Th2;

            hence contradiction by A15, A16, A18, XBOOLE_0:def 5;

          end;

          hence (( MergeSequence (p,q1)) . i) = (( MergeSequence (p,q2)) . i) by A14, A18, Th3;

        end;

      end;

      ( len ( MergeSequence (p,q2))) = ( len p) by Def1;

      hence contradiction by A3, A8, A9, A10, A12, FINSEQ_2: 9;

    end;

    definition

      let X be set;

      let Y be finite Subset-Family of X;

      :: YELLOW15:def3

      attr Y is in_general_position means not {} in ( Components Y);

    end

    theorem :: YELLOW15:20

    for X be set holds for Y,Z be finite Subset-Family of X st Z is in_general_position & Y c= Z holds Y is in_general_position

    proof

      let X be set;

      let Y,Z be finite Subset-Family of X such that

       A1: Z is in_general_position and

       A2: Y c= Z;

      

       A3: not {} in ( Components Z) by A1;

       not {} in ( Components Y)

      proof

        deffunc T( set) = TRUE ;

        consider p be FinSequence of ( bool X) such that

         A4: ( len p) = ( card Y) and

         A5: ( rng p) = Y and

         A6: ( Components Y) = { ( Intersect ( rng ( MergeSequence (p,q)))) where q be FinSequence of BOOLEAN : ( len q) = ( len p) } by Def2;

        

         A7: p is one-to-one by A4, A5, FINSEQ_4: 62;

        then

         A8: ( rng p) = ( dom (p " )) by FUNCT_1: 33;

        consider p1 be FinSequence of ( bool X) such that

         A9: ( len p1) = ( card Z) and

         A10: ( rng p1) = Z and

         A11: ( Components Z) = { ( Intersect ( rng ( MergeSequence (p1,q)))) where q be FinSequence of BOOLEAN : ( len q) = ( len p1) } by Def2;

        defpred C[ set] means (p1 . $1) in ( rng p);

        assume {} in ( Components Y);

        then

        consider q be FinSequence of BOOLEAN such that

         A12: {} = ( Intersect ( rng ( MergeSequence (p,q)))) and

         A13: ( len q) = ( len p) by A6;

        deffunc F( set) = (((q * (p " )) * p1) . $1);

        

         A14: ( dom p) = ( rng (p " )) by A7, FUNCT_1: 33;

        

         A15: for i be Nat st i in ( Seg ( len p1)) holds ( C[i] implies F(i) in BOOLEAN ) & ( not C[i] implies T(i) in BOOLEAN )

        proof

          let i be Nat;

          assume i in ( Seg ( len p1));

          then

           A16: i in ( dom p1) by FINSEQ_1:def 3;

          thus (p1 . i) in ( rng p) implies (((q * (p " )) * p1) . i) in BOOLEAN

          proof

            assume

             A17: (p1 . i) in ( rng p);

            ( rng (p " )) = ( dom q) by A13, A14, FINSEQ_3: 29;

            then (p1 . i) in ( dom (q * (p " ))) by A8, A17, RELAT_1: 27;

            then

             A18: ((q * (p " )) . (p1 . i)) in ( rng (q * (p " ))) by FUNCT_1:def 3;

            ( dom (q * (p " ))) c= ( rng p) by A8, RELAT_1: 25;

            then ( rng (q * (p " ))) = ( rng ((q * (p " )) * p1)) by A2, A5, A10, RELAT_1: 28, XBOOLE_1: 1;

            then (((q * (p " )) * p1) . i) in ( rng ((q * (p " )) * p1)) by A16, A18, FUNCT_1: 13;

            hence thesis;

          end;

          thus thesis;

        end;

        consider q1 be FinSequence of BOOLEAN such that

         A19: ( len q1) = ( len p1) and

         A20: for i be Nat st i in ( Seg ( len p1)) holds ( C[i] implies (q1 . i) = F(i)) & ( not C[i] implies (q1 . i) = T(i)) from SeqLambda1C( A15);

        

         A21: p1 is one-to-one by A9, A10, FINSEQ_4: 62;

        then

         A22: ( rng p1) = ( dom (p1 " )) by FUNCT_1: 33;

        ( rng ( MergeSequence (p,q))) c= ( rng ( MergeSequence (p1,q1)))

        proof

          let z be object;

          assume z in ( rng ( MergeSequence (p,q)));

          then

          consider i be Nat such that

           A23: i in ( dom ( MergeSequence (p,q))) and

           A24: (( MergeSequence (p,q)) . i) = z by FINSEQ_2: 10;

          i in ( Seg ( len ( MergeSequence (p,q)))) by A23, FINSEQ_1:def 3;

          then i in ( Seg ( len p)) by Def1;

          then

           A25: i in ( dom p) by FINSEQ_1:def 3;

          then

           A26: i in ( dom ((p1 " ) * p)) by A2, A5, A10, A22, RELAT_1: 27;

          then (((p1 " ) * p) . i) in ( rng ((p1 " ) * p)) by FUNCT_1:def 3;

          then

           A27: (((p1 " ) * p) . i) in ( rng (p1 " )) by FUNCT_1: 14;

          then

           A28: (((p1 " ) * p) . i) in ( dom p1) by A21, FUNCT_1: 33;

          then

          reconsider j = (((p1 " ) * p) . i) as Element of NAT ;

          (p1 . j) = ((p1 * ((p1 " ) * p)) . i) by A26, FUNCT_1: 13

          .= (((p1 * (p1 " )) * p) . i) by RELAT_1: 36

          .= ((( id ( rng p1)) * p) . i) by A21, FUNCT_1: 39

          .= (p . i) by A2, A5, A10, RELAT_1: 53;

          then

           A29: (p1 . j) in ( rng p) by A25, FUNCT_1:def 3;

          j in ( Seg ( len p1)) by A28, FINSEQ_1:def 3;

          

          then

           A30: (q1 . j) = (((q * (p " )) * p1) . (((p1 " ) * p) . i)) by A20, A29

          .= ((((q * (p " )) * p1) * ((p1 " ) * p)) . i) by A26, FUNCT_1: 13

          .= (((q * (p " )) * (p1 * ((p1 " ) * p))) . i) by RELAT_1: 36

          .= (((q * (p " )) * ((p1 * (p1 " )) * p)) . i) by RELAT_1: 36

          .= (((q * (p " )) * (( id ( rng p1)) * p)) . i) by A21, FUNCT_1: 39

          .= (((q * (p " )) * p) . i) by A2, A5, A10, RELAT_1: 53

          .= ((q * ((p " ) * p)) . i) by RELAT_1: 36

          .= ((q * ( id ( dom p))) . i) by A7, FUNCT_1: 39

          .= ((q * ( id ( dom q))) . i) by A13, FINSEQ_3: 29

          .= (q . i) by RELAT_1: 52;

          

           A31: j in ( dom p1) by A21, A27, FUNCT_1: 33;

           A32:

          now

            per cases by XBOOLEAN:def 3;

              suppose

               A33: (q . i) = TRUE ;

              

              hence z = (p . i) by A24, Th2

              .= ((( id ( rng p1)) * p) . i) by A2, A5, A10, RELAT_1: 53

              .= (((p1 * (p1 " )) * p) . i) by A21, FUNCT_1: 39

              .= ((p1 * ((p1 " ) * p)) . i) by RELAT_1: 36

              .= (p1 . j) by A26, FUNCT_1: 13

              .= (( MergeSequence (p1,q1)) . j) by A30, A33, Th2;

            end;

              suppose

               A34: (q . i) = FALSE ;

              

              hence z = (X \ (p . i)) by A24, A25, Th3

              .= (X \ ((( id ( rng p1)) * p) . i)) by A2, A5, A10, RELAT_1: 53

              .= (X \ (((p1 * (p1 " )) * p) . i)) by A21, FUNCT_1: 39

              .= (X \ ((p1 * ((p1 " ) * p)) . i)) by RELAT_1: 36

              .= (X \ (p1 . j)) by A26, FUNCT_1: 13

              .= (( MergeSequence (p1,q1)) . j) by A31, A30, A34, Th3;

            end;

          end;

          j in ( dom ( MergeSequence (p1,q1))) by A28, Th1;

          hence thesis by A32, FUNCT_1:def 3;

        end;

        then {} = ( Intersect ( rng ( MergeSequence (p1,q1)))) by A12, SETFAM_1: 44, XBOOLE_1: 3;

        hence contradiction by A3, A11, A19;

      end;

      hence thesis;

    end;

    theorem :: YELLOW15:21

    for X be non empty set holds for Y be empty Subset-Family of X holds Y is in_general_position

    proof

      let X be non empty set;

      let Y be empty Subset-Family of X;

       not {} in {X} by TARSKI:def 1;

      then not {} in ( Components Y) by Th13;

      hence thesis;

    end;

    theorem :: YELLOW15:22

    for X be non empty set holds for Y be finite Subset-Family of X st Y is in_general_position holds ( Components Y) is a_partition of X

    proof

      let X be non empty set;

      let Y be finite Subset-Family of X;

      assume Y is in_general_position;

      then

       A1: for A be Subset of X st A in ( Components Y) holds A <> {} & for B be Subset of X st B in ( Components Y) holds A = B or A misses B by Th16;

      ( union ( Components Y)) = X by Th15;

      hence thesis by A1, EQREL_1:def 4;

    end;

    begin

    theorem :: YELLOW15:23

    

     Th20: for L be non empty RelStr holds ( [#] L) is infs-closed sups-closed

    proof

      let L be non empty RelStr;

      for X be Subset of ( [#] L) st ex_inf_of (X,L) holds ( "/\" (X,L)) in ( [#] L);

      hence ( [#] L) is infs-closed by WAYBEL23: 19;

      for X be Subset of ( [#] L) st ex_sup_of (X,L) holds ( "\/" (X,L)) in ( [#] L);

      hence thesis by WAYBEL23: 20;

    end;

    theorem :: YELLOW15:24

    

     Th21: for L be non empty RelStr holds ( [#] L) is with_bottom with_top

    proof

      let L be non empty RelStr;

      ( Bottom L) in ( [#] L);

      hence ( [#] L) is with_bottom by WAYBEL23:def 8;

      ( Top L) in ( [#] L);

      hence thesis by WAYBEL23:def 9;

    end;

    registration

      let L be non empty RelStr;

      cluster ( [#] L) -> infs-closed sups-closed with_bottom with_top;

      coherence by Th20, Th21;

    end

    theorem :: YELLOW15:25

    for L be continuous sup-Semilattice holds ( [#] L) is CLbasis of L

    proof

      let L be continuous sup-Semilattice;

      now

        let x be Element of L;

        (( waybelow x) /\ ( [#] L)) = ( waybelow x) by XBOOLE_1: 28;

        hence x = ( sup (( waybelow x) /\ ( [#] L))) by WAYBEL_3:def 5;

      end;

      hence thesis by WAYBEL23:def 7;

    end;

    theorem :: YELLOW15:26

    for L be up-complete non empty Poset st L is finite holds the carrier of L = the carrier of ( CompactSublatt L)

    proof

      let L be up-complete non empty Poset;

      assume

       A1: L is finite;

      

       A2: the carrier of L c= the carrier of ( CompactSublatt L)

      proof

        let z be object;

        assume z in the carrier of L;

        then

        reconsider z1 = z as Element of L;

        z1 is compact by A1, WAYBEL_3: 17;

        hence thesis by WAYBEL_8:def 1;

      end;

      the carrier of ( CompactSublatt L) c= the carrier of L by YELLOW_0:def 13;

      hence thesis by A2;

    end;

    theorem :: YELLOW15:27

    for L be lower-bounded sup-Semilattice holds for B be Subset of L st B is infinite holds ( card B) = ( card ( finsups B))

    proof

      let L be lower-bounded sup-Semilattice;

      let B be Subset of L;

      defpred P[ Function, set] means $2 = ( "\/" (( rng $1),L));

      assume

       A1: B is infinite;

      then

      reconsider B1 = B as non empty Subset of L;

      

       A2: for p be Element of (B1 * ) holds ex u be Element of ( finsups B1) st P[p, u]

      proof

        let p be Element of (B1 * );

        

         A3: ( rng p) c= the carrier of L by XBOOLE_1: 1;

        now

          per cases ;

            suppose ( rng p) is empty;

            hence ex_sup_of (( rng p),L) by YELLOW_0: 42;

          end;

            suppose ( rng p) is non empty;

            hence ex_sup_of (( rng p),L) by A3, YELLOW_0: 54;

          end;

        end;

        then ( "\/" (( rng p),L)) in { ( "\/" (Y,L)) where Y be finite Subset of B1 : ex_sup_of (Y,L) };

        then

        reconsider u = ( "\/" (( rng p),L)) as Element of ( finsups B1) by WAYBEL_0:def 27;

        take u;

        thus thesis;

      end;

      consider f be Function of (B1 * ), ( finsups B1) such that

       A4: for p be Element of (B1 * ) holds P[p, (f . p)] from FUNCT_2:sch 3( A2);

      B c= ( finsups B)

      proof

        let z be object;

        assume

         A5: z in B;

        then

        reconsider z1 = z as Element of L;

        

         A6: {z1} c= B by A5, TARSKI:def 1;

         ex_sup_of ( {z1},L) & z = ( sup {z1}) by YELLOW_0: 38, YELLOW_0: 39;

        then z1 in { ( "\/" (Y,L)) where Y be finite Subset of B : ex_sup_of (Y,L) } by A6;

        hence thesis by WAYBEL_0:def 27;

      end;

      then

       A7: ( card B) c= ( card ( finsups B)) by CARD_1: 11;

      

       A8: ( dom f) = (B1 * ) by FUNCT_2:def 1;

      ( finsups B) c= ( rng f)

      proof

        let z be object;

        assume z in ( finsups B);

        then z in { ( "\/" (Y,L)) where Y be finite Subset of B : ex_sup_of (Y,L) } by WAYBEL_0:def 27;

        then

        consider Y be finite Subset of B such that

         A9: z = ( "\/" (Y,L)) and ex_sup_of (Y,L);

        consider p be FinSequence such that

         A10: ( rng p) = Y by FINSEQ_1: 52;

        reconsider p as FinSequence of B1 by A10, FINSEQ_1:def 4;

        reconsider p1 = p as Element of (B1 * ) by FINSEQ_1:def 11;

        (f . p1) = ( "\/" (( rng p1),L)) by A4;

        hence thesis by A8, A9, A10, FUNCT_1:def 3;

      end;

      then ( card ( finsups B1)) c= ( card (B1 * )) by A8, CARD_1: 12;

      then ( card ( finsups B1)) c= ( card B1) by A1, CARD_4: 24;

      hence thesis by A7;

    end;

    theorem :: YELLOW15:28

    for T be T_0 non empty TopSpace holds ( card the carrier of T) c= ( card the topology of T)

    proof

      let T be T_0 non empty TopSpace;

      defpred P[ Element of T, set] means $2 = (( [#] T) \ ( Cl {$1}));

      

       A1: for e be Element of T holds ex u be Element of the topology of T st P[e, u]

      proof

        let e be Element of T;

        reconsider u = (( [#] T) \ ( Cl {e})) as Element of the topology of T by PRE_TOPC:def 2, PRE_TOPC:def 3;

        take u;

        thus thesis;

      end;

      consider f be Function of the carrier of T, the topology of T such that

       A2: for e be Element of T holds P[e, (f . e)] from FUNCT_2:sch 3( A1);

      

       A3: f is one-to-one

      proof

        let x1,x2 be object;

        assume that

         A4: x1 in ( dom f) & x2 in ( dom f) and

         A5: (f . x1) = (f . x2);

        reconsider y1 = x1, y2 = x2 as Element of T by A4;

        (( Cl {y1}) ` ) = (( [#] T) \ ( Cl {y1})) by SUBSET_1:def 4

        .= (f . x2) by A2, A5

        .= (( [#] T) \ ( Cl {y2})) by A2

        .= (( Cl {y2}) ` ) by SUBSET_1:def 4;

        then ( Cl {y2}) c= ( Cl {y1}) & ( Cl {y1}) c= ( Cl {y2}) by SUBSET_1: 12;

        hence thesis by XBOOLE_0:def 10, YELLOW_8: 23;

      end;

      ( dom f) = the carrier of T & ( rng f) c= the topology of T by FUNCT_2:def 1;

      hence thesis by A3, CARD_1: 10;

    end;

    theorem :: YELLOW15:29

    

     Th26: for T be TopStruct holds for X be Subset of T st X is open holds for B be finite Subset-Family of T st B is Basis of T holds for Y be set st Y in ( Components B) holds X misses Y or Y c= X

    proof

      let T be TopStruct;

      let X be Subset of T;

      assume X is open;

      then

       A1: X in the topology of T by PRE_TOPC:def 2;

      let B be finite Subset-Family of T;

      assume B is Basis of T;

      then the topology of T c= ( UniCl B) by CANTOR_1:def 2;

      then

      consider Z be Subset-Family of T such that

       A2: Z c= B and

       A3: X = ( union Z) by A1, CANTOR_1:def 1;

      let Y be set;

      consider p be FinSequence of ( bool the carrier of T) such that ( len p) = ( card B) and

       A4: ( rng p) = B and

       A5: ( Components B) = { ( Intersect ( rng ( MergeSequence (p,q)))) where q be FinSequence of BOOLEAN : ( len q) = ( len p) } by Def2;

      assume Y in ( Components B);

      then

      consider q be FinSequence of BOOLEAN such that

       A6: Y = ( Intersect ( rng ( MergeSequence (p,q)))) and ( len q) = ( len p) by A5;

      assume (X /\ Y) <> {} ;

      then

      consider x be object such that

       A7: x in (X /\ Y) by XBOOLE_0:def 1;

      x in X by A7, XBOOLE_0:def 4;

      then

      consider b be set such that

       A8: x in b and

       A9: b in Z by A3, TARSKI:def 4;

      

       A10: x in Y by A7, XBOOLE_0:def 4;

      

       A11: Y c= b

      proof

        let z be object;

        consider i be Nat such that

         A12: i in ( dom p) and

         A13: (p . i) = b by A4, A2, A9, FINSEQ_2: 10;

        

         A14: i in ( dom ( MergeSequence (p,q))) by A12, Th1;

        now

          per cases by XBOOLEAN:def 3;

            suppose (q . i) = TRUE ;

            hence (( MergeSequence (p,q)) . i) = b by A13, Th2;

          end;

            suppose (q . i) = FALSE ;

            then

             A15: (( MergeSequence (p,q)) . i) = (the carrier of T \ b) by A12, A13, Th3;

            (( MergeSequence (p,q)) . i) in ( rng ( MergeSequence (p,q))) by A14, FUNCT_1:def 3;

            then Y c= (the carrier of T \ b) by A6, A15, MSSUBFAM: 2;

            hence (( MergeSequence (p,q)) . i) = b by A10, A8, XBOOLE_0:def 5;

          end;

        end;

        then

         A16: b in ( rng ( MergeSequence (p,q))) by A14, FUNCT_1:def 3;

        assume z in Y;

        hence thesis by A6, A16, SETFAM_1: 43;

      end;

      b c= X by A3, A9, ZFMISC_1: 74;

      hence thesis by A11;

    end;

    theorem :: YELLOW15:30

    for T be T_0 TopSpace st T is infinite holds for B be Basis of T holds B is infinite

    proof

      let T be T_0 TopSpace;

      assume

       A1: T is infinite;

      let B be Basis of T;

      assume B is finite;

      then

      reconsider B1 = B as finite Subset-Family of T;

      ( union ( Components B1)) = the carrier of T by Th15;

      then

      consider X be set such that

       A2: X in ( Components B1) and

       A3: X is infinite by A1, FINSET_1: 7;

      reconsider X as infinite set by A3;

      consider x be object such that

       A4: x in X by XBOOLE_0:def 1;

      consider y be object such that

       A5: y in X and

       A6: x <> y by A4, SUBSET_1: 48;

      reconsider x1 = x, y1 = y as Element of T by A2, A4, A5;

      consider Y be Subset of T such that

       A7: Y is open and

       A8: x1 in Y & not y1 in Y or y1 in Y & not x1 in Y by A1, A6, T_0TOPSP:def 7;

      now

        per cases by A8;

          suppose

           A9: x in Y & not y in Y;

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

          then X c= Y by A2, A7, Th26, XBOOLE_0: 4;

          hence contradiction by A5, A9;

        end;

          suppose

           A10: y in Y & not x in Y;

          then y in (Y /\ X) by A5, XBOOLE_0:def 4;

          then X c= Y by A2, A7, Th26, XBOOLE_0: 4;

          hence contradiction by A4, A10;

        end;

      end;

      hence contradiction;

    end;

    theorem :: YELLOW15:31

    for T be non empty TopSpace st T is finite holds for B be Basis of T holds for x be Element of T holds ( meet { A where A be Element of the topology of T : x in A }) in B

    proof

      deffunc F( set) = $1;

      let T be non empty TopSpace;

      assume T is finite;

      then

      reconsider tT = the topology of T as finite non empty set;

      let B be Basis of T;

      let x be Element of T;

      defpred P[ set] means x in $1;

      { A where A be Element of the topology of T : x in A } c= ( bool the carrier of T)

      proof

        let z be object;

        assume z in { A where A be Element of the topology of T : x in A };

        then ex A be Element of the topology of T st z = A & x in A;

        hence thesis;

      end;

      then

      reconsider sfA = { A where A be Element of the topology of T : x in A } as Subset-Family of T;

      reconsider sfA as Subset-Family of T;

       A1:

      now

        let Y be set;

        assume Y in sfA;

        then ex A be Element of the topology of T st Y = A & x in A;

        hence x in Y;

      end;

      the carrier of T is Element of the topology of T by PRE_TOPC:def 1;

      then the carrier of T in sfA;

      then

       A2: x in ( meet sfA) by A1, SETFAM_1:def 1;

       A3:

      now

        let P be Subset of T;

        assume P in sfA;

        then ex A be Element of the topology of T st P = A & x in A;

        hence P is open by PRE_TOPC:def 2;

      end;

      { F(A) where A be Element of tT : P[A] } is finite from PRE_CIRC:sch 1;

      then ( meet sfA) is open by A3, TOPS_2: 20, TOPS_2:def 1;

      then

      consider a be Subset of T such that

       A4: a in B and

       A5: x in a and

       A6: a c= ( meet sfA) by A2, YELLOW_9: 31;

      ( meet sfA) c= a

      proof

        let z be object;

        B c= the topology of T by TOPS_2: 64;

        then a in sfA by A4, A5;

        hence thesis by SETFAM_1:def 1;

      end;

      hence thesis by A4, A6, XBOOLE_0:def 10;

    end;