yellow_9.miz



    begin

    scheme :: YELLOW_9:sch1

    FraenkelInvolution { A() -> non empty set , X,Y() -> Subset of A() , F( set) -> Element of A() } :

X() = { F(a) where a be Element of A() : a in Y() }

      provided

       A1: Y() = { F(a) where a be Element of A() : a in X() }

       and

       A2: for a be Element of A() holds F(F) = a;

      hereby

        let x be object;

        assume

         A3: x in X();

        then

        reconsider a = x as Element of A();

        

         A4: F(a) in Y() by A1, A3;

        F(F) = a by A2;

        hence x in { F(b) where b be Element of A() : b in Y() } by A4;

      end;

      let x be object;

      assume x in { F(b) where b be Element of A() : b in Y() };

      then

      consider b be Element of A() such that

       A5: x = F(b) and

       A6: b in Y();

      ex a be Element of A() st (b = F(a)) & (a in X()) by A1, A6;

      hence thesis by A2, A5;

    end;

    scheme :: YELLOW_9:sch2

    FraenkelComplement1 { A() -> non empty RelStr , X() -> Subset-Family of A() , Y() -> set , F( set) -> Subset of A() } :

( COMPLEMENT X()) = { (F(a) ` ) where a be Element of A() : a in Y() }

      provided

       A1: X() = { F(a) where a be Element of A() : a in Y() };

      hereby

        let x be object;

        assume

         A2: x in ( COMPLEMENT X());

        then

        reconsider y = x as Subset of A();

        (y ` ) in X() by A2, SETFAM_1:def 7;

        then

         A3: ex b be Element of A() st ((y ` ) = F(b)) & (b in Y()) by A1;

        x = ((y ` ) ` );

        hence x in { (F(a) ` ) where a be Element of A() : a in Y() } by A3;

      end;

      let x be object;

      assume x in { (F(a) ` ) where a be Element of A() : a in Y() };

      then

      consider a be Element of A() such that

       A4: x = (F(a) ` ) and

       A5: a in Y();

      F(a) in X() by A1, A5;

      hence thesis by A4, YELLOW_8: 5;

    end;

    scheme :: YELLOW_9:sch3

    FraenkelComplement2 { A() -> non empty RelStr , X() -> Subset-Family of A() , Y() -> set , F( set) -> Subset of A() } :

( COMPLEMENT X()) = { F(a) where a be Element of A() : a in Y() }

      provided

       A1: X() = { (F(a) ` ) where a be Element of A() : a in Y() };

      hereby

        let x be object;

        assume

         A2: x in ( COMPLEMENT X());

        then

        reconsider y = x as Subset of A();

        (y ` ) in X() by A2, SETFAM_1:def 7;

        then

         A3: ex b be Element of A() st ((y ` ) = (F(b) ` )) & (b in Y()) by A1;

        x = ((y ` ) ` );

        hence x in { F(a) where a be Element of A() : a in Y() } by A3;

      end;

      let x be object;

      assume x in { F(a) where a be Element of A() : a in Y() };

      then

      consider a be Element of A() such that

       A4: x = F(a) and

       A5: a in Y();

      (F(a) ` ) in X() by A1, A5;

      hence thesis by A4, SETFAM_1:def 7;

    end;

    theorem :: YELLOW_9:1

    for R be non empty RelStr, x,y be Element of R holds y in (( uparrow x) ` ) iff not x <= y

    proof

      let R be non empty RelStr, x,y be Element of R;

      (( uparrow x) ` ) = (the carrier of R \ ( uparrow x)) by SUBSET_1:def 4;

      then y in (( uparrow x) ` ) iff not y in ( uparrow x) by XBOOLE_0:def 5;

      hence thesis by WAYBEL_0: 18;

    end;

    scheme :: YELLOW_9:sch4

    ABC { A() -> TopSpace , F( set) -> set , f() -> Function , P[ set] } :

(f() " ( union { F(x) where x be Subset of A() : P[x] })) = ( union { (f() " F(y)) where y be Subset of A() : P[y] });

      set X = { F(x) where x be Subset of A() : P[x] };

      set Y = { (f() " F(y)) where y be Subset of A() : P[y] };

      hereby

        let x be object;

        assume

         A1: x in (f() " ( union X));

        then

         A2: x in ( dom f()) by FUNCT_1:def 7;

        (f() . x) in ( union X) by A1, FUNCT_1:def 7;

        then

        consider y be set such that

         A3: (f() . x) in y and

         A4: y in X by TARSKI:def 4;

        consider a be Subset of A() such that

         A5: y = F(a) and

         A6: P[a] by A4;

        

         A7: x in (f() " F(a)) by A2, A3, A5, FUNCT_1:def 7;

        (f() " F(a)) in Y by A6;

        hence x in ( union Y) by A7, TARSKI:def 4;

      end;

      let x be object;

      assume x in ( union Y);

      then

      consider y be set such that

       A8: x in y and

       A9: y in Y by TARSKI:def 4;

      consider a be Subset of A() such that

       A10: y = (f() " F(a)) and

       A11: P[a] by A9;

      

       A12: (f() . x) in F(a) by A8, A10, FUNCT_1:def 7;

      F(a) in X by A11;

      then

       A13: (f() . x) in ( union X) by A12, TARSKI:def 4;

      x in ( dom f()) by A8, A10, FUNCT_1:def 7;

      hence thesis by A13, FUNCT_1:def 7;

    end;

    theorem :: YELLOW_9:2

    

     Th2: for S be 1-sorted, T be non empty 1-sorted, f be Function of S, T holds for X be Subset of T holds ((f " X) ` ) = (f " (X ` ))

    proof

      let S be 1-sorted, T be non empty 1-sorted, f be Function of S, T;

      let X be Subset of T;

      

      thus ((f " X) ` ) = (the carrier of S \ (f " X)) by SUBSET_1:def 4

      .= ((f " the carrier of T) \ (f " X)) by FUNCT_2: 40

      .= (f " (the carrier of T \ X)) by FUNCT_1: 69

      .= (f " (X ` )) by SUBSET_1:def 4;

    end;

    theorem :: YELLOW_9:3

    

     Th3: for T be 1-sorted, F be Subset-Family of T holds ( COMPLEMENT F) = { (a ` ) where a be Subset of T : a in F }

    proof

      let T be 1-sorted, F be Subset-Family of T;

      set X = { (a ` ) where a be Subset of T : a in F };

      hereby

        let x be object;

        assume

         A1: x in ( COMPLEMENT F);

        then

        reconsider P = x as Subset of T;

        

         A2: (P ` ) in F by A1, SETFAM_1:def 7;

        ((P ` ) ` ) = P;

        hence x in X by A2;

      end;

      let x be object;

      assume x in X;

      then ex P be Subset of T st x = (P ` ) & P in F;

      hence thesis by YELLOW_8: 5;

    end;

    theorem :: YELLOW_9:4

    

     Th4: for R be non empty RelStr holds for F be Subset of R holds ( uparrow F) = ( union { ( uparrow x) where x be Element of R : x in F }) & ( downarrow F) = ( union { ( downarrow x) where x be Element of R : x in F })

    proof

      let R be non empty RelStr, F be Subset of R;

      

       A1: ( uparrow F) = { x where x be Element of R : ex y be Element of R st x >= y & y in F } by WAYBEL_0: 15;

      

       A2: ( downarrow F) = { x where x be Element of R : ex y be Element of R st x <= y & y in F } by WAYBEL_0: 14;

      hereby

        let a be object;

        assume a in ( uparrow F);

        then

        consider x be Element of R such that

         A3: a = x and

         A4: ex y be Element of R st x >= y & y in F by A1;

        consider y be Element of R such that

         A5: x >= y and

         A6: y in F by A4;

        

         A7: ( uparrow y) in { ( uparrow z) where z be Element of R : z in F } by A6;

        x in ( uparrow y) by A5, WAYBEL_0: 18;

        hence a in ( union { ( uparrow z) where z be Element of R : z in F }) by A3, A7, TARSKI:def 4;

      end;

      hereby

        let a be object;

        assume a in ( union { ( uparrow x) where x be Element of R : x in F });

        then

        consider X be set such that

         A8: a in X and

         A9: X in { ( uparrow x) where x be Element of R : x in F } by TARSKI:def 4;

        consider x be Element of R such that

         A10: X = ( uparrow x) and

         A11: x in F by A9;

        reconsider y = a as Element of R by A8, A10;

        y >= x by A8, A10, WAYBEL_0: 18;

        hence a in ( uparrow F) by A1, A11;

      end;

      hereby

        let a be object;

        assume a in ( downarrow F);

        then

        consider x be Element of R such that

         A12: a = x and

         A13: ex y be Element of R st x <= y & y in F by A2;

        consider y be Element of R such that

         A14: x <= y and

         A15: y in F by A13;

        

         A16: ( downarrow y) in { ( downarrow z) where z be Element of R : z in F } by A15;

        x in ( downarrow y) by A14, WAYBEL_0: 17;

        hence a in ( union { ( downarrow z) where z be Element of R : z in F }) by A12, A16, TARSKI:def 4;

      end;

      hereby

        let a be object;

        assume a in ( union { ( downarrow x) where x be Element of R : x in F });

        then

        consider X be set such that

         A17: a in X and

         A18: X in { ( downarrow x) where x be Element of R : x in F } by TARSKI:def 4;

        consider x be Element of R such that

         A19: X = ( downarrow x) and

         A20: x in F by A18;

        reconsider y = a as Element of R by A17, A19;

        y <= x by A17, A19, WAYBEL_0: 17;

        hence a in ( downarrow F) by A2, A20;

      end;

    end;

    theorem :: YELLOW_9:5

    for R be non empty RelStr holds for A be Subset-Family of R, F be Subset of R st A = { (( uparrow x) ` ) where x be Element of R : x in F } holds ( Intersect A) = (( uparrow F) ` )

    proof

      let R be non empty RelStr;

      deffunc F( Element of R) = ( uparrow $1);

      let A be Subset-Family of R, F be Subset of R such that

       A1: A = { ( F(x) ` ) where x be Element of R : x in F };

      

       A2: ( COMPLEMENT A) = { F(x) where x be Element of R : x in F } from FraenkelComplement2( A1);

      reconsider C = ( COMPLEMENT A) as Subset-Family of R;

      ( COMPLEMENT C) = A;

      

      hence ( Intersect A) = (( union C) ` ) by YELLOW_8: 6

      .= (( uparrow F) ` ) by A2, Th4;

    end;

    registration

      cluster strict complete1 -element for TopLattice;

      existence

      proof

        take the strict reflexive1 -element discrete finite TopRelStr;

        thus thesis;

      end;

    end

    registration

      let S be non empty RelStr, T be upper-bounded non empty reflexive antisymmetric RelStr;

      cluster infs-preserving for Function of S, T;

      existence

      proof

        take f = (S --> ( Top T));

        let A be Subset of S;

        assume ex_inf_of (A,S);

        

         A1: ( rng f) = {( Top T)} by FUNCOP_1: 8;

        (f .: A) c= ( rng f) by RELAT_1: 111;

        then

         A2: (f .: A) = {} or (f .: A) = {( Top T)} by A1, ZFMISC_1: 33;

        hence ex_inf_of ((f .: A),T) by YELLOW_0: 38, YELLOW_0: 43;

        

        thus ( inf (f .: A)) = ( Top T) by A2, YELLOW_0: 39

        .= (f . ( inf A)) by FUNCOP_1: 7;

      end;

    end

    registration

      let S be non empty RelStr, T be lower-bounded non empty reflexive antisymmetric RelStr;

      cluster sups-preserving for Function of S, T;

      existence

      proof

        take f = (S --> ( Bottom T));

        let A be Subset of S;

        assume ex_sup_of (A,S);

        

         A1: ( rng f) = {( Bottom T)} by FUNCOP_1: 8;

        (f .: A) c= ( rng f) by RELAT_1: 111;

        then

         A2: (f .: A) = {} or (f .: A) = {( Bottom T)} by A1, ZFMISC_1: 33;

        hence ex_sup_of ((f .: A),T) by YELLOW_0: 38, YELLOW_0: 42;

        

        thus ( sup (f .: A)) = ( Bottom T) by A2, YELLOW_0: 39

        .= (f . ( sup A)) by FUNCOP_1: 7;

      end;

    end

    definition

      let R,S be 1-sorted;

      assume

       A1: the carrier of S c= the carrier of R;

      

       A2: ( dom ( id the carrier of S)) = the carrier of S;

      

       A3: ( rng ( id the carrier of S)) = the carrier of S;

      :: YELLOW_9:def1

      func incl (S,R) -> Function of S, R equals

      : Def1: ( id the carrier of S);

      coherence by A1, A2, A3, FUNCT_2: 2;

    end

    registration

      let R be non empty RelStr;

      let S be non empty SubRelStr of R;

      cluster ( incl (S,R)) -> monotone;

      coherence

      proof

        let x,y be Element of S;

        reconsider a = x, b = y as Element of R by YELLOW_0: 58;

        the carrier of S c= the carrier of R by YELLOW_0:def 13;

        then

         A1: ( incl (S,R)) = ( id the carrier of S) by Def1;

        then

         A2: (( incl (S,R)) . x) = a;

        (( incl (S,R)) . y) = b by A1;

        hence thesis by A2, YELLOW_0: 59;

      end;

    end

    definition

      let R be non empty RelStr, X be non empty Subset of R;

      :: YELLOW_9:def2

      func X +id -> strict non empty NetStr over R equals (( incl (( subrelstr X),R)) * (( subrelstr X) +id ));

      coherence ;

      :: YELLOW_9:def3

      func X opp+id -> strict non empty NetStr over R equals (( incl (( subrelstr X),R)) * (( subrelstr X) opp+id ));

      coherence ;

    end

    theorem :: YELLOW_9:6

    for R be non empty RelStr, X be non empty Subset of R holds the carrier of (X +id ) = X & (X +id ) is full SubRelStr of R & for x be Element of (X +id ) holds ((X +id ) . x) = x

    proof

      let R be non empty RelStr, X be non empty Subset of R;

      

       A1: the RelStr of (X +id ) = the RelStr of (( subrelstr X) +id ) by WAYBEL_9:def 8;

      

       A2: the mapping of (X +id ) = (( incl (( subrelstr X),R)) * the mapping of (( subrelstr X) +id )) by WAYBEL_9:def 8;

      

       A3: the carrier of ( subrelstr X) = X by YELLOW_0:def 15;

      hence

       A4: the carrier of (X +id ) = X by A1, WAYBEL_9:def 5;

      

       A5: the RelStr of (( subrelstr X) +id ) = ( subrelstr X) by WAYBEL_9:def 5;

      the InternalRel of ( subrelstr X) c= the InternalRel of R by YELLOW_0:def 13;

      then

      reconsider S = (X +id ) as SubRelStr of R by A1, A3, A5, YELLOW_0:def 13;

      the InternalRel of S = (the InternalRel of R |_2 the carrier of S) by A1, A5, YELLOW_0:def 14;

      hence (X +id ) is full SubRelStr of R by YELLOW_0:def 14;

      let x be Element of (X +id );

      ( id ( subrelstr X)) = ( id X) by YELLOW_0:def 15;

      then

       A6: the mapping of (( subrelstr X) +id ) = ( id X) by WAYBEL_9:def 5;

      

       A7: ( dom ( id X)) = X;

      ( incl (( subrelstr X),R)) = ( id X) by A3, Def1;

      then the mapping of (X +id ) = ( id X) by A2, A6, A7, RELAT_1: 52;

      hence thesis by A4;

    end;

    theorem :: YELLOW_9:7

    for R be non empty RelStr, X be non empty Subset of R holds the carrier of (X opp+id ) = X & (X opp+id ) is full SubRelStr of (R opp ) & for x be Element of (X opp+id ) holds ((X opp+id ) . x) = x

    proof

      let R be non empty RelStr, X be non empty Subset of R;

      

       A1: the RelStr of (X opp+id ) = the RelStr of (( subrelstr X) opp+id ) by WAYBEL_9:def 8;

      

       A2: the mapping of (X opp+id ) = (( incl (( subrelstr X),R)) * the mapping of (( subrelstr X) opp+id )) by WAYBEL_9:def 8;

      

       A3: the carrier of ( subrelstr X) = X by YELLOW_0:def 15;

      

       A4: the carrier of (( subrelstr X) opp+id ) = the carrier of ( subrelstr X) by WAYBEL_9:def 6;

      

       A5: the InternalRel of (( subrelstr X) opp+id ) = (the InternalRel of ( subrelstr X) ~ ) by WAYBEL_9:def 6;

      thus the carrier of (X opp+id ) = X by A1, A3, WAYBEL_9:def 6;

      

       A6: (R opp ) = RelStr (# the carrier of R, (the InternalRel of R ~ ) #) by LATTICE3:def 5;

      the InternalRel of ( subrelstr X) = (the InternalRel of R |_2 X) by A3, YELLOW_0:def 14;

      then

       A7: the InternalRel of (( subrelstr X) opp+id ) = ((the InternalRel of R ~ ) |_2 X) by A5, ORDERS_1: 83;

      then the InternalRel of (( subrelstr X) opp+id ) c= the InternalRel of (R opp ) by A6, XBOOLE_1: 17;

      then

      reconsider S = (X opp+id ) as SubRelStr of (R opp ) by A1, A3, A4, A6, YELLOW_0:def 13;

      the InternalRel of S = (the InternalRel of (R opp ) |_2 the carrier of S) by A1, A4, A6, A7, YELLOW_0:def 15;

      hence (X opp+id ) is full SubRelStr of (R opp ) by YELLOW_0:def 14;

      let x be Element of (X opp+id );

      ( id ( subrelstr X)) = ( id X) by YELLOW_0:def 15;

      then

       A8: the mapping of (( subrelstr X) opp+id ) = ( id X) by WAYBEL_9:def 6;

      

       A9: ( dom ( id X)) = X;

      ( incl (( subrelstr X),R)) = ( id X) by A3, Def1;

      then the mapping of (X opp+id ) = ( id X) by A2, A8, A9, RELAT_1: 52;

      hence thesis by A1, A3, A4;

    end;

    registration

      let R be non empty reflexive RelStr;

      let X be non empty Subset of R;

      cluster (X +id ) -> reflexive;

      coherence ;

      cluster (X opp+id ) -> reflexive;

      coherence ;

    end

    registration

      let R be non empty transitive RelStr;

      let X be non empty Subset of R;

      cluster (X +id ) -> transitive;

      coherence ;

      cluster (X opp+id ) -> transitive;

      coherence ;

    end

    registration

      let R be non empty reflexive RelStr;

      let I be directed Subset of R;

      cluster ( subrelstr I) -> directed;

      coherence

      proof

        let x,y be Element of ( subrelstr I);

        

         A1: the carrier of ( subrelstr I) = I by YELLOW_0:def 15;

        assume that

         A2: x in ( [#] ( subrelstr I)) and

         A3: y in ( [#] ( subrelstr I));

        reconsider a = x, b = y as Element of R by A1, A2, A3;

        consider c be Element of R such that

         A4: c in I and

         A5: a <= c and

         A6: b <= c by A1, A2, WAYBEL_0:def 1;

        reconsider z = c as Element of ( subrelstr I) by A4, YELLOW_0:def 15;

        take z;

        thus thesis by A2, A5, A6, YELLOW_0: 60;

      end;

    end

    registration

      let R be non empty reflexive RelStr;

      let I be directed non empty Subset of R;

      cluster (I +id ) -> directed;

      coherence ;

    end

    registration

      let R be non empty reflexive RelStr;

      let F be filtered non empty Subset of R;

      cluster (( subrelstr F) opp+id ) -> directed;

      coherence

      proof

        set I = F, A = (( subrelstr I) opp+id );

        let x,y be Element of (( subrelstr I) opp+id );

        

         A1: the carrier of ( subrelstr I) = I by YELLOW_0:def 15;

        

         A2: the carrier of A = the carrier of ( subrelstr F) by WAYBEL_9:def 6;

        assume that

         A3: x in ( [#] A) and

         A4: y in ( [#] A);

        reconsider a = x, b = y as Element of R by A1, A2, A3, A4;

        

         A5: the RelStr of A = the RelStr of (( subrelstr F) opp ) by WAYBEL_9: 11;

        consider c be Element of R such that

         A6: c in I and

         A7: a >= c and

         A8: b >= c by A1, A2, WAYBEL_0:def 2;

        reconsider a1 = x, b1 = y, c1 = c as Element of ( subrelstr F) by A6, WAYBEL_9:def 6, YELLOW_0:def 15;

        reconsider z = c as Element of A by A2, A6, YELLOW_0:def 15;

        take z;

        

         A9: (a1 ~ ) = a1 by LATTICE3:def 6;

        

         A10: (b1 ~ ) = b1 by LATTICE3:def 6;

        

         A11: (c1 ~ ) = c1 by LATTICE3:def 6;

        

         A12: a1 >= c1 by A7, YELLOW_0: 60;

        

         A13: b1 >= c1 by A8, YELLOW_0: 60;

        

         A14: (a1 ~ ) <= (c1 ~ ) by A12, LATTICE3: 9;

        (b1 ~ ) <= (c1 ~ ) by A13, LATTICE3: 9;

        hence thesis by A5, A9, A10, A11, A14;

      end;

    end

    registration

      let R be non empty reflexive RelStr;

      let F be filtered non empty Subset of R;

      cluster (F opp+id ) -> directed;

      coherence ;

    end

    begin

    theorem :: YELLOW_9:8

    

     Th8: for T be TopSpace st T is empty holds the topology of T = { {} }

    proof

      let T1 be TopSpace;

      assume T1 is empty;

      then

       A1: the carrier of T1 = {} ;

      then {} in the topology of T1 by PRE_TOPC:def 1;

      hence thesis by A1, ZFMISC_1: 1, ZFMISC_1: 33;

    end;

    theorem :: YELLOW_9:9

    

     Th9: for T be 1 -element TopSpace holds the topology of T = ( bool the carrier of T) & for x be Point of T holds the carrier of T = {x} & the topology of T = { {} , {x}}

    proof

      let T be 1 -element TopSpace;

      thus the topology of T c= ( bool the carrier of T);

      consider x be Point of T such that

       A1: the carrier of T = {x} by TEX_1:def 1;

      

       A2: {} in the topology of T by PRE_TOPC: 1;

      

       A3: the carrier of T in the topology of T by PRE_TOPC:def 1;

      

       A4: ( bool {x}) = { {} , {x}} by ZFMISC_1: 24;

      hence ( bool the carrier of T) c= the topology of T by A1, A2, A3, ZFMISC_1: 32;

      let a be Point of T;

      a = x by STRUCT_0:def 10;

      hence the carrier of T = {a} & the topology of T c= { {} , {a}} & { {} , {a}} c= the topology of T by A1, A2, A3, A4, ZFMISC_1: 32;

    end;

    theorem :: YELLOW_9:10

    for T be 1 -element TopSpace holds {the carrier of T} is Basis of T & {} is prebasis of T & { {} } is prebasis of T

    proof

      let T be 1 -element TopSpace;

      set BB = {the carrier of T};

      

       A1: the carrier of T c= the carrier of T;

      

       A2: the topology of T = ( bool the carrier of T) by Th9;

      reconsider BB as Subset-Family of T by A1, ZFMISC_1: 31;

      set x = the Element of T;

      

       A3: the topology of T = { {} , {x}} by Th9;

      

       A4: the carrier of T = {x} by Th9;

      

       A5: {} c= ( bool the carrier of T);

      

       A6: {} c= BB;

      

       A7: {} c= the carrier of T;

      reconsider C = {} as Subset-Family of T by XBOOLE_1: 2;

      the topology of T c= ( UniCl BB)

      proof

        let a be object;

        assume a in the topology of T;

        then a = {x} & ( union { {x}}) = {x} & BB c= BB & BB c= ( bool the carrier of T) or a = {} by A3, TARSKI:def 2, ZFMISC_1: 25;

        hence thesis by A4, A5, A6, A7, CANTOR_1:def 1, ZFMISC_1: 2;

      end;

      hence

       A8: {the carrier of T} is Basis of T by A2, CANTOR_1:def 2, TOPS_2: 64;

      

       A9: {} c= the topology of T;

      BB c= ( FinMeetCl C)

      proof

        let x be object;

        assume x in BB;

        then x = the carrier of T by TARSKI:def 1;

        then ( Intersect C) = x by SETFAM_1:def 9;

        hence thesis by CANTOR_1:def 3;

      end;

      hence {} is prebasis of T by A8, A9, CANTOR_1:def 4, TOPS_2: 64;

       {} c= the carrier of T;

      then

      reconsider D = { {} } as Subset-Family of T by ZFMISC_1: 31;

      

       A10: D c= the topology of T by A3, ZFMISC_1: 7;

      BB c= ( FinMeetCl D)

      proof

        let x be object;

        assume x in BB;

        then

         A11: x = the carrier of T by TARSKI:def 1;

        

         A12: ( Intersect C) = the carrier of T by SETFAM_1:def 9;

        C c= D;

        hence thesis by A11, A12, CANTOR_1:def 3;

      end;

      hence thesis by A8, A10, CANTOR_1:def 4, TOPS_2: 64;

    end;

    theorem :: YELLOW_9:11

    

     Th11: for X,Y be set, A be Subset-Family of X st A = {Y} holds ( FinMeetCl A) = {Y, X} & ( UniCl A) = {Y, {} }

    proof

      let X,Z be set, A be Subset-Family of X such that

       A1: A = {Z};

      thus ( FinMeetCl A) c= {Z, X}

      proof

        let x be object;

        assume x in ( FinMeetCl A);

        then

        consider Y be Subset-Family of X such that

         A2: Y c= A and Y is finite and

         A3: x = ( Intersect Y) by CANTOR_1:def 3;

        Y = {} or Y = {Z} by A1, A2, ZFMISC_1: 33;

        then x = X or x = ( meet {Z}) by A3, SETFAM_1:def 9;

        then x = X or x = Z by SETFAM_1: 10;

        hence thesis by TARSKI:def 2;

      end;

      reconsider E = {} as Subset-Family of X by XBOOLE_1: 2;

      reconsider E as Subset-Family of X;

      hereby

        let x be object;

        assume x in {Z, X};

        then x = X or x = Z by TARSKI:def 2;

        then x = X or x = ( meet {Z}) by SETFAM_1: 10;

        then x = ( Intersect E) & E c= A or x = ( Intersect A) & A c= A by A1, SETFAM_1:def 9;

        hence x in ( FinMeetCl A) by A1, CANTOR_1:def 3;

      end;

      hereby

        let x be object;

        assume x in ( UniCl A);

        then

        consider Y be Subset-Family of X such that

         A4: Y c= A and

         A5: x = ( union Y) by CANTOR_1:def 1;

        Y = {} or Y = {Z} by A1, A4, ZFMISC_1: 33;

        then x = {} or x = Z by A5, ZFMISC_1: 2, ZFMISC_1: 25;

        hence x in {Z, {} } by TARSKI:def 2;

      end;

      let x be object;

      assume x in {Z, {} };

      then x = {} or x = Z by TARSKI:def 2;

      then x = ( union E) & E c= A or x = ( union A) & A c= A by A1, ZFMISC_1: 2, ZFMISC_1: 25;

      hence thesis by CANTOR_1:def 1;

    end;

    theorem :: YELLOW_9:12

    for X be set, A,B be Subset-Family of X st A = (B \/ {X}) or B = (A \ {X}) holds ( Intersect A) = ( Intersect B)

    proof

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

      assume

       A1: A = (B \/ {X}) or B = (A \ {X});

      hereby

        let x be object;

        assume

         A2: x in ( Intersect A);

        now

          let y be set;

          assume y in B;

          then y in A by A1, XBOOLE_0:def 3, XBOOLE_0:def 5;

          hence x in y by A2, SETFAM_1: 43;

        end;

        hence x in ( Intersect B) by A2, SETFAM_1: 43;

      end;

      let x be object;

      assume

       A3: x in ( Intersect B);

      now

        let y be set;

        assume y in A;

        then y in B & not y in {X} or y in {X} by A1, XBOOLE_0:def 3, XBOOLE_0:def 5;

        then y in B or y = X by TARSKI:def 1;

        hence x in y by A3, SETFAM_1: 43;

      end;

      hence thesis by A3, SETFAM_1: 43;

    end;

    theorem :: YELLOW_9:13

    for X be set, A,B be Subset-Family of X st A = (B \/ {X}) or B = (A \ {X}) holds ( FinMeetCl A) = ( FinMeetCl B)

    proof

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

      assume

       A1: A = (B \/ {X}) or B = (A \ {X});

      X in ( FinMeetCl B) by CANTOR_1: 8;

      then

       A2: {X} c= ( FinMeetCl B) by ZFMISC_1: 31;

      

       A3: B c= ( FinMeetCl B) by CANTOR_1: 4;

      ((A \ {X}) \/ {X}) = (A \/ {X}) by XBOOLE_1: 39;

      then

       A4: A c= (B \/ {X}) by A1, XBOOLE_1: 7;

      (B \/ {X}) c= ( FinMeetCl B) by A2, A3, XBOOLE_1: 8;

      then A c= ( FinMeetCl B) by A4;

      then ( FinMeetCl A) c= ( FinMeetCl ( FinMeetCl B)) by CANTOR_1: 14;

      hence ( FinMeetCl A) c= ( FinMeetCl B) by CANTOR_1: 11;

      thus thesis by A1, CANTOR_1: 14, XBOOLE_1: 7, XBOOLE_1: 36;

    end;

    theorem :: YELLOW_9:14

    

     Th14: for X be set, A be Subset-Family of X st X in A holds for x be set holds x in ( FinMeetCl A) iff ex Y be finite non empty Subset-Family of X st Y c= A & x = ( Intersect Y)

    proof

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

      assume

       A1: X in A;

      then

       A2: {X} c= A by ZFMISC_1: 31;

      reconsider Z = {X} as finite non empty Subset-Family of X by A1, ZFMISC_1: 31;

      reconsider Z as finite non empty Subset-Family of X;

      

       A3: ( Intersect Z) = ( meet Z) by SETFAM_1:def 9

      .= X by SETFAM_1: 10;

      let x be set;

      hereby

        assume x in ( FinMeetCl A);

        then

        consider Y be Subset-Family of X such that

         A4: Y c= A and

         A5: Y is finite and

         A6: x = ( Intersect Y) by CANTOR_1:def 3;

        per cases ;

          suppose Y = {} ;

          then x = X by A6, SETFAM_1:def 9;

          hence ex Y be finite non empty Subset-Family of X st Y c= A & x = ( Intersect Y) by A2, A3;

        end;

          suppose Y <> {} ;

          hence ex Y be finite non empty Subset-Family of X st Y c= A & x = ( Intersect Y) by A4, A5, A6;

        end;

      end;

      thus thesis by CANTOR_1:def 3;

    end;

    theorem :: YELLOW_9:15

    

     Th15: for X be set, A be Subset-Family of X holds ( UniCl ( UniCl A)) = ( UniCl A)

    proof

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

      hereby

        let x be object;

        reconsider xx = x as set by TARSKI: 1;

        assume x in ( UniCl ( UniCl A));

        then

        consider Y be Subset-Family of X such that

         A1: Y c= ( UniCl A) and

         A2: x = ( union Y) by CANTOR_1:def 1;

        set Z = { y where y be Subset of X : y in A & y c= xx };

        Z c= ( bool X)

        proof

          let a be object;

          assume a in Z;

          then ex y be Subset of X st a = y & y in A & y c= xx;

          hence thesis;

        end;

        then

        reconsider Z as Subset-Family of X;

        

         A3: xx = ( union Z)

        proof

          hereby

            let a be object;

            assume a in xx;

            then

            consider s be set such that

             A4: a in s and

             A5: s in Y by A2, TARSKI:def 4;

            consider t be Subset-Family of X such that

             A6: t c= A and

             A7: s = ( union t) by A1, A5, CANTOR_1:def 1;

            consider u be set such that

             A8: a in u and

             A9: u in t by A4, A7, TARSKI:def 4;

            reconsider u as Subset of X by A9;

            

             A10: u c= s by A7, A9, ZFMISC_1: 74;

            s c= xx by A2, A5, ZFMISC_1: 74;

            then u c= xx by A10;

            then u in Z by A6, A9;

            hence a in ( union Z) by A8, TARSKI:def 4;

          end;

          let a be object;

          assume a in ( union Z);

          then

          consider u be set such that

           A11: a in u and

           A12: u in Z by TARSKI:def 4;

          ex y be Subset of X st u = y & y in A & y c= xx by A12;

          hence thesis by A11;

        end;

        Z c= A

        proof

          let a be object;

          assume a in Z;

          then ex y be Subset of X st a = y & y in A & y c= xx;

          hence thesis;

        end;

        hence x in ( UniCl A) by A3, CANTOR_1:def 1;

      end;

      thus thesis by CANTOR_1: 1;

    end;

    theorem :: YELLOW_9:16

    

     Th16: for X be set, A be empty Subset-Family of X holds ( UniCl A) = { {} }

    proof

      let X be set, A be empty Subset-Family of X;

      hereby

        let x be object;

        assume x in ( UniCl A);

        then

        consider B be Subset-Family of X such that

         A1: B c= A and

         A2: x = ( union B) by CANTOR_1:def 1;

        B = {} by A1;

        hence x in { {} } by A2, TARSKI:def 1, ZFMISC_1: 2;

      end;

      let x be object;

      assume x in { {} };

      then

       A3: x = {} by TARSKI:def 1;

      ( union ( {} ( bool X))) = {} by ZFMISC_1: 2;

      hence thesis by A3, CANTOR_1:def 1;

    end;

    theorem :: YELLOW_9:17

    

     Th17: for X be set, A be empty Subset-Family of X holds ( FinMeetCl A) = {X}

    proof

      let X be set, A be empty Subset-Family of X;

      hereby

        let x be object;

        assume x in ( FinMeetCl A);

        then

        consider B be Subset-Family of X such that

         A1: B c= A and B is finite and

         A2: x = ( Intersect B) by CANTOR_1:def 3;

        B = {} by A1;

        then x = X by A2, SETFAM_1:def 9;

        hence x in {X} by TARSKI:def 1;

      end;

      let x be object;

      assume x in {X};

      then

       A3: x = X by TARSKI:def 1;

      ( Intersect ( {} ( bool X))) = X by SETFAM_1:def 9;

      hence thesis by A3, CANTOR_1:def 3;

    end;

    theorem :: YELLOW_9:18

    

     Th18: for X be set, A be Subset-Family of X st A = { {} , X} holds ( UniCl A) = A & ( FinMeetCl A) = A

    proof

      let X be set, A be Subset-Family of X such that

       A1: A = { {} , X};

      hereby

        let a be object;

        assume a in ( UniCl A);

        then

        consider y be Subset-Family of X such that

         A2: y c= A and

         A3: a = ( union y) by CANTOR_1:def 1;

        y = {} or y = { {} } or y = {X} or y = { {} , X} by A1, A2, ZFMISC_1: 36;

        then a = {} or a = X or a = ( {} \/ X) & ( {} \/ X) = X by A3, ZFMISC_1: 2, ZFMISC_1: 25, ZFMISC_1: 75;

        hence a in A by A1, TARSKI:def 2;

      end;

      thus A c= ( UniCl A) by CANTOR_1: 1;

      hereby

        let a be object;

        assume a in ( FinMeetCl A);

        then

        consider y be Subset-Family of X such that

         A4: y c= A and y is finite and

         A5: a = ( Intersect y) by CANTOR_1:def 3;

        y = {} or y = { {} } or y = {X} or y = { {} , X} by A1, A4, ZFMISC_1: 36;

        then a = X or a = ( meet { {} }) or a = ( meet {X}) or a = ( meet { {} , X}) by A5, SETFAM_1:def 9;

        then a = X or a = {} or a = ( {} /\ X) & ( {} /\ X) = {} by SETFAM_1: 10, SETFAM_1: 11;

        hence a in A by A1, TARSKI:def 2;

      end;

      thus thesis by CANTOR_1: 4;

    end;

    theorem :: YELLOW_9:19

    

     Th19: for X,Y be set, A be Subset-Family of X, B be Subset-Family of Y holds (A c= B implies ( UniCl A) c= ( UniCl B)) & (A = B implies ( UniCl A) = ( UniCl B))

    proof

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

       A1:

      now

        let X,Y be set;

        let A be Subset-Family of X, B be Subset-Family of Y such that

         A2: A c= B;

        thus ( UniCl A) c= ( UniCl B)

        proof

          let x be object;

          assume x in ( UniCl A);

          then

          consider y be Subset-Family of X such that

           A3: y c= A and

           A4: x = ( union y) by CANTOR_1:def 1;

          y c= B by A2, A3;

          then y is Subset-Family of Y by XBOOLE_1: 1;

          then ex y be Subset-Family of Y st y c= B & x = ( union y) by A2, A3, A4, XBOOLE_1: 1;

          hence thesis by CANTOR_1:def 1;

        end;

      end;

      hence A c= B implies ( UniCl A) c= ( UniCl B);

      assume A = B;

      hence ( UniCl A) c= ( UniCl B) & ( UniCl B) c= ( UniCl A) by A1;

    end;

    theorem :: YELLOW_9:20

    

     Th20: for X,Y be set, A be Subset-Family of X, B be Subset-Family of Y st A = B & X in A holds ( FinMeetCl B) = ( {Y} \/ ( FinMeetCl A))

    proof

      let X,Y be set, A be Subset-Family of X, B be Subset-Family of Y such that

       A1: A = B and

       A2: X in A;

      thus ( FinMeetCl B) c= ( {Y} \/ ( FinMeetCl A))

      proof

        let x be object;

        assume x in ( FinMeetCl B);

        then

        consider y be Subset-Family of Y such that

         A3: y c= B and

         A4: y is finite and

         A5: x = ( Intersect y) by CANTOR_1:def 3;

        reconsider z = y as Subset-Family of X by A1, A3, XBOOLE_1: 1;

        reconsider z as Subset-Family of X;

        per cases ;

          suppose y = {} ;

          then x = Y by A5, SETFAM_1:def 9;

          then x in {Y} by TARSKI:def 1;

          hence thesis by XBOOLE_0:def 3;

        end;

          suppose

           A6: y <> {} ;

          then

           A7: ( Intersect y) = ( meet y) by SETFAM_1:def 9;

          ( Intersect z) = ( meet y) by A6, SETFAM_1:def 9;

          then x in ( FinMeetCl A) by A1, A3, A4, A5, A7, CANTOR_1:def 3;

          hence thesis by XBOOLE_0:def 3;

        end;

      end;

      let x be object;

      assume

       A8: x in ( {Y} \/ ( FinMeetCl A));

      per cases by A8, XBOOLE_0:def 3;

        suppose x in {Y};

        then

         A9: x = Y by TARSKI:def 1;

        

         A10: ( Intersect ( {} ( bool Y))) = Y by SETFAM_1:def 9;

        ( {} ( bool Y)) c= B;

        hence thesis by A9, A10, CANTOR_1:def 3;

      end;

        suppose x in ( FinMeetCl A);

        then

        consider y be non empty finite Subset-Family of X such that

         A11: y c= A and

         A12: x = ( Intersect y) by A2, Th14;

        reconsider z = y as Subset-Family of Y by A1, A11, XBOOLE_1: 1;

        reconsider z as Subset-Family of Y;

        x = ( meet z) by A12, SETFAM_1:def 9

        .= ( Intersect z) by SETFAM_1:def 9;

        hence thesis by A1, A11, CANTOR_1:def 3;

      end;

    end;

    theorem :: YELLOW_9:21

    

     Th21: for X be set, A be Subset-Family of X holds ( UniCl ( FinMeetCl ( UniCl A))) = ( UniCl ( FinMeetCl A))

    proof

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

      per cases ;

        suppose

         A1: A = {} ;

        then

         A2: ( FinMeetCl A) = {X} by Th17;

        ( UniCl A) = { {} } by A1, Th16;

        then

         A3: ( FinMeetCl ( UniCl A)) = { {} , X} by Th11;

        ( UniCl ( FinMeetCl A)) = {X, {} } by A2, Th11;

        hence thesis by A3, Th18;

      end;

        suppose A <> {} ;

        then

        reconsider A as non empty Subset-Family of X;

        

         A4: ( UniCl ( FinMeetCl ( UniCl A))) c= ( UniCl ( UniCl ( FinMeetCl A)))

        proof

          let x be object;

          assume x in ( UniCl ( FinMeetCl ( UniCl A)));

          then

          consider Y be Subset-Family of X such that

           A5: Y c= ( FinMeetCl ( UniCl A)) and

           A6: x = ( union Y) by CANTOR_1:def 1;

          Y c= ( UniCl ( FinMeetCl A))

          proof

            let y be object;

            reconsider yy = y as set by TARSKI: 1;

            assume y in Y;

            then

            consider Z be Subset-Family of X such that

             A7: Z c= ( UniCl A) and

             A8: Z is finite and

             A9: y = ( Intersect Z) by A5, CANTOR_1:def 3;

            per cases ;

              suppose Z = {} ;

              then y = X by A9, SETFAM_1:def 9;

              then

               A10: y in ( FinMeetCl A) by CANTOR_1: 8;

              ( FinMeetCl A) c= ( UniCl ( FinMeetCl A)) by CANTOR_1: 1;

              hence thesis by A10;

            end;

              suppose

               A11: Z <> {} ;

              then

               A12: y = ( meet Z) by A9, SETFAM_1:def 9;

              set G = { ( meet ( rng f)) where f be Element of ( Funcs (Z,A)) : for z be set st z in Z holds (f . z) c= z };

              

               A13: G c= ( FinMeetCl A)

              proof

                let a be object;

                assume a in G;

                then

                consider f be Element of ( Funcs (Z,A)) such that

                 A14: a = ( meet ( rng f)) and for z be set st z in Z holds (f . z) c= z;

                reconsider B = ( rng f) as Subset-Family of X by XBOOLE_1: 1;

                reconsider B as Subset-Family of X;

                ( Intersect B) = a by A11, A14, SETFAM_1:def 9;

                hence thesis by A8, CANTOR_1:def 3;

              end;

              then

              reconsider G as Subset-Family of X by XBOOLE_1: 1;

              reconsider G as Subset-Family of X;

              ( union G) = yy

              proof

                hereby

                  let a be object;

                  assume a in ( union G);

                  then

                  consider b be set such that

                   A15: a in b and

                   A16: b in G by TARSKI:def 4;

                  consider f be Element of ( Funcs (Z,A)) such that

                   A17: b = ( meet ( rng f)) and

                   A18: for z be set st z in Z holds (f . z) c= z by A16;

                  

                   A19: ( dom f) = Z by FUNCT_2:def 1;

                  reconsider B = ( rng f) as Subset-Family of X by XBOOLE_1: 1;

                  reconsider B as Subset-Family of X;

                  b c= yy

                  proof

                    let c be object;

                    assume

                     A20: c in b;

                    now

                      let d be set;

                      assume

                       A21: d in Z;

                      then (f . d) in B by A19, FUNCT_1:def 3;

                      then

                       A22: b c= (f . d) by A17, SETFAM_1: 3;

                      

                       A23: (f . d) c= d by A18, A21;

                      c in (f . d) by A20, A22;

                      hence c in d by A23;

                    end;

                    hence thesis by A11, A12, SETFAM_1:def 1;

                  end;

                  hence a in yy by A15;

                end;

                let a be object;

                assume

                 A24: a in yy;

                defpred P[ object, object] means ex A,B be set st A = $1 & B = $2 & a in B & B c= A;

                 A25:

                now

                  let z be object;

                  assume

                   A26: z in Z;

                  reconsider zz = z as set by TARSKI: 1;

                  

                   A27: a in zz by A12, A24, SETFAM_1:def 1, A26;

                  consider C be Subset-Family of X such that

                   A28: C c= A and

                   A29: z = ( union C) by A7, A26, CANTOR_1:def 1;

                  consider w be set such that

                   A30: a in w and

                   A31: w in C by A27, A29, TARSKI:def 4;

                  reconsider w as object;

                  take w;

                  thus w in A by A28, A31;

                  thus P[z, w] by A29, A30, A31, ZFMISC_1: 74;

                end;

                consider f be Function such that

                 A32: ( dom f) = Z & ( rng f) c= A and

                 A33: for z be object st z in Z holds P[z, (f . z)] from FUNCT_1:sch 6( A25);

                reconsider f as Element of ( Funcs (Z,A)) by A32, FUNCT_2:def 2;

                for z be set st z in Z holds (f . z) c= z

                proof

                  let z be set;

                  assume z in Z;

                  then P[z, (f . z)] by A33;

                  hence thesis;

                end;

                then

                 A34: ( meet ( rng f)) in G;

                now

                  thus ( rng f) <> {} by A11;

                  let y be set;

                  assume y in ( rng f);

                  then

                  consider z be object such that

                   A35: z in Z & y = (f . z) by A32, FUNCT_1:def 3;

                   P[z, (f . z)] by A33, A35;

                  hence a in y by A35;

                end;

                then a in ( meet ( rng f)) by SETFAM_1:def 1;

                hence thesis by A34, TARSKI:def 4;

              end;

              hence thesis by A13, CANTOR_1:def 1;

            end;

          end;

          hence thesis by A6, CANTOR_1:def 1;

        end;

        ( FinMeetCl A) c= ( FinMeetCl ( UniCl A)) by CANTOR_1: 1, CANTOR_1: 14;

        then

         A36: ( UniCl ( FinMeetCl A)) c= ( UniCl ( FinMeetCl ( UniCl A))) by CANTOR_1: 9;

        ( UniCl ( UniCl ( FinMeetCl A))) = ( UniCl ( FinMeetCl A)) by Th15;

        hence thesis by A4, A36;

      end;

    end;

    begin

    theorem :: YELLOW_9:22

    

     Th22: for T be TopSpace, K be Subset-Family of T holds the topology of T = ( UniCl K) iff K is Basis of T

    proof

      let T be TopSpace, K be Subset-Family of T;

      thus the topology of T = ( UniCl K) implies K is Basis of T by CANTOR_1: 1, CANTOR_1:def 2, TOPS_2: 64;

      assume

       A1: K is Basis of T;

      then K c= the topology of T by TOPS_2: 64;

      then

       A2: ( UniCl K) c= ( UniCl the topology of T) by CANTOR_1: 9;

      the topology of T c= ( UniCl K) by A1, CANTOR_1:def 2;

      hence the topology of T c= ( UniCl K) & ( UniCl K) c= the topology of T by A2, CANTOR_1: 6;

    end;

    theorem :: YELLOW_9:23

    

     Th23: for T be TopSpace, K be Subset-Family of T holds K is prebasis of T iff ( FinMeetCl K) is Basis of T

    proof

      let T be TopSpace, BB be Subset-Family of T;

      

       A1: T is empty implies the topology of T = ( bool the carrier of T) by ZFMISC_1: 1, Th8;

      thus BB is prebasis of T implies ( FinMeetCl BB) is Basis of T

      proof

        assume

         A2: BB is prebasis of T;

        then BB c= the topology of T by TOPS_2: 64;

        then ( FinMeetCl BB) c= ( FinMeetCl the topology of T) by CANTOR_1: 14;

        then

         A3: ( FinMeetCl BB) c= the topology of T by A1, CANTOR_1: 5;

        consider A be Basis of T such that

         A4: A c= ( FinMeetCl BB) by A2, CANTOR_1:def 4;

        

         A5: the topology of T c= ( UniCl A) by CANTOR_1:def 2;

        ( UniCl A) c= ( UniCl ( FinMeetCl BB)) by A4, CANTOR_1: 9;

        then the topology of T c= ( UniCl ( FinMeetCl BB)) by A5;

        hence thesis by A3, CANTOR_1:def 2, TOPS_2: 64;

      end;

      assume

       A6: ( FinMeetCl BB) is Basis of T;

      

       A7: BB c= ( FinMeetCl BB) by CANTOR_1: 4;

      ( FinMeetCl BB) c= the topology of T by A6, TOPS_2: 64;

      then BB c= the topology of T by A7;

      hence thesis by A6, CANTOR_1:def 4, TOPS_2: 64;

    end;

    theorem :: YELLOW_9:24

    

     Th24: for T be non empty TopSpace, B be Subset-Family of T st ( UniCl B) is prebasis of T holds B is prebasis of T

    proof

      let T be non empty TopSpace, B be Subset-Family of T;

      assume ( UniCl B) is prebasis of T;

      then ( FinMeetCl ( UniCl B)) is Basis of T by Th23;

      then ( UniCl ( FinMeetCl ( UniCl B))) = the topology of T by Th22;

      then ( UniCl ( FinMeetCl B)) = the topology of T by Th21;

      then ( FinMeetCl B) is Basis of T by Th22;

      hence thesis by Th23;

    end;

    theorem :: YELLOW_9:25

    

     Th25: for T1,T2 be TopSpace, B be Basis of T1 st the carrier of T1 = the carrier of T2 & B is Basis of T2 holds the topology of T1 = the topology of T2

    proof

      let T1,T2 be TopSpace, B be Basis of T1;

      assume that

       A1: the carrier of T1 = the carrier of T2 and

       A2: B is Basis of T2;

      reconsider C = B as Basis of T2 by A2;

      

      thus the topology of T1 = ( UniCl C) by A1, Th22

      .= the topology of T2 by Th22;

    end;

    theorem :: YELLOW_9:26

    

     Th26: for T1,T2 be TopSpace, P be prebasis of T1 st the carrier of T1 = the carrier of T2 & P is prebasis of T2 holds the topology of T1 = the topology of T2

    proof

      let T1,T2 be TopSpace, P be prebasis of T1;

      assume that

       A1: the carrier of T1 = the carrier of T2 and

       A2: P is prebasis of T2;

      reconsider C = P as prebasis of T2 by A2;

      

       A3: ( FinMeetCl P) is Basis of T1 by Th23;

      ( FinMeetCl C) is Basis of T2 by Th23;

      hence thesis by A1, A3, Th25;

    end;

    theorem :: YELLOW_9:27

    for T be TopSpace, K be Basis of T holds K is open & K is prebasis of T;

    theorem :: YELLOW_9:28

    for T be TopSpace, K be prebasis of T holds K is open;

    theorem :: YELLOW_9:29

    

     Th29: for T be non empty TopSpace, B be prebasis of T holds (B \/ {the carrier of T}) is prebasis of T

    proof

      let T be non empty TopSpace, B be prebasis of T;

      set C = (B \/ {the carrier of T});

      

       A1: the carrier of T in the topology of T by PRE_TOPC:def 1;

      

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

      

       A3: {the carrier of T} c= the topology of T by A1, ZFMISC_1: 31;

      then C c= the topology of T by A2, XBOOLE_1: 8;

      then

      reconsider C as Subset-Family of T by XBOOLE_1: 1;

      

       A4: C c= the topology of T by A2, A3, XBOOLE_1: 8;

      

       A5: ( FinMeetCl B) c= ( FinMeetCl C) by CANTOR_1: 14, XBOOLE_1: 7;

      ( FinMeetCl B) is Basis of T by Th23;

      hence thesis by A4, A5, CANTOR_1:def 4, TOPS_2: 64;

    end;

    theorem :: YELLOW_9:30

    for T be TopSpace, B be Basis of T holds (B \/ {the carrier of T}) is Basis of T

    proof

      let T be TopSpace, B be Basis of T;

      set C = (B \/ {the carrier of T});

      

       A1: the carrier of T in the topology of T by PRE_TOPC:def 1;

      

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

      

       A3: {the carrier of T} c= the topology of T by A1, ZFMISC_1: 31;

      then C c= the topology of T by A2, XBOOLE_1: 8;

      then

      reconsider C as Subset-Family of T by XBOOLE_1: 1;

      

       A4: C c= the topology of T by A2, A3, XBOOLE_1: 8;

      

       A5: ( UniCl B) c= ( UniCl C) by CANTOR_1: 9, XBOOLE_1: 7;

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

      then the topology of T c= ( UniCl C) by A5;

      hence thesis by A4, CANTOR_1:def 2, TOPS_2: 64;

    end;

    theorem :: YELLOW_9:31

    

     Th31: for T be TopSpace, B be Basis of T holds for A be Subset of T holds A is open iff for p be Point of T st p in A holds ex a be Subset of T st a in B & p in a & a c= A

    proof

      let T be TopSpace, K be Basis of T, A be Subset of T;

      hereby

        assume A is open;

        then

         A1: A = ( union { G where G be Subset of T : G in K & G c= A }) by YELLOW_8: 9;

        let p be Point of T;

        assume p in A;

        then

        consider Z be set such that

         A2: p in Z and

         A3: Z in { G where G be Subset of T : G in K & G c= A } by A1, TARSKI:def 4;

        ex a be Subset of T st Z = a & a in K & a c= A by A3;

        hence ex a be Subset of T st a in K & p in a & a c= A by A2;

      end;

      assume

       A4: for p be Point of T st p in A holds ex a be Subset of T st a in K & p in a & a c= A;

      set F = { G where G be Subset of T : G in K & G c= A };

      F c= ( bool the carrier of T)

      proof

        let x be object;

        assume x in F;

        then ex G be Subset of T st x = G & G in K & G c= A;

        hence thesis;

      end;

      then

      reconsider F as Subset-Family of T;

      reconsider F as Subset-Family of T;

      

       A5: F is open

      proof

        let x be Subset of T;

        assume x in F;

        then

         A6: ex G be Subset of T st x = G & G in K & G c= A;

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

        hence x in the topology of T by A6;

      end;

      A = ( union F)

      proof

        hereby

          let x be object;

          assume

           A7: x in A;

          then

          reconsider p = x as Point of T;

          consider a be Subset of T such that

           A8: a in K and

           A9: p in a and

           A10: a c= A by A4, A7;

          a in F by A8, A10;

          hence x in ( union F) by A9, TARSKI:def 4;

        end;

        F c= ( bool A)

        proof

          let x be object;

          assume x in F;

          then ex G be Subset of T st x = G & G in K & G c= A;

          hence thesis;

        end;

        then ( union F) c= ( union ( bool A)) by ZFMISC_1: 77;

        hence thesis by ZFMISC_1: 81;

      end;

      hence thesis by A5, TOPS_2: 19;

    end;

    theorem :: YELLOW_9:32

    

     Th32: for T be TopSpace, B be Subset-Family of T st B c= the topology of T & for A be Subset of T st A is open holds for p be Point of T st p in A holds ex a be Subset of T st a in B & p in a & a c= A holds B is Basis of T

    proof

      let T be TopSpace, B be Subset-Family of T such that

       A1: B c= the topology of T and

       A2: for A be Subset of T st A is open holds for p be Point of T st p in A holds ex a be Subset of T st a in B & p in a & a c= A;

      

       A3: B is open by A1, TOPS_2: 64;

      B is quasi_basis

      proof

        let x be object;

        assume

         A4: x in the topology of T;

        then

        reconsider A = x as Subset of T;

        set Y = { V where V be Subset of T : V in B & V c= A };

        Y c= ( bool the carrier of T)

        proof

          let y be object;

          assume y in Y;

          then ex V be Subset of T st y = V & V in B & V c= A;

          hence thesis;

        end;

        then

        reconsider Y as Subset-Family of T;

        

         A5: Y c= B

        proof

          let y be object;

          assume y in Y;

          then ex V be Subset of T st y = V & V in B & V c= A;

          hence thesis;

        end;

        A = ( union Y)

        proof

          hereby

            let p be object;

            assume

             A6: p in A;

            then p in A;

            then

            reconsider q = p as Point of T;

            A is open by A4;

            then

            consider a be Subset of T such that

             A7: a in B and

             A8: q in a and

             A9: a c= A by A2, A6;

            a in Y by A7, A9;

            hence p in ( union Y) by A8, TARSKI:def 4;

          end;

          let p be object;

          assume p in ( union Y);

          then

          consider a be set such that

           A10: p in a and

           A11: a in Y by TARSKI:def 4;

          ex V be Subset of T st a = V & V in B & V c= A by A11;

          hence thesis by A10;

        end;

        hence thesis by A5, CANTOR_1:def 1;

      end;

      hence thesis by A3;

    end;

    theorem :: YELLOW_9:33

    

     Th33: for S be TopSpace, T be non empty TopSpace, K be Basis of T holds for f be Function of S, T holds f is continuous iff for A be Subset of T st A in K holds (f " (A ` )) is closed

    proof

      let S be TopSpace, T be non empty TopSpace, BB be Basis of T, f be Function of S, T;

      

       A1: BB c= the topology of T by TOPS_2: 64;

      hereby

        assume

         A2: f is continuous;

        let A be Subset of T;

        assume A in BB;

        then A is open by A1;

        then (A ` ) is closed by TOPS_1: 4;

        hence (f " (A ` )) is closed by A2;

      end;

      assume

       A3: for A be Subset of T st A in BB holds (f " (A ` )) is closed;

      let A be Subset of T;

      assume A is closed;

      then (A ` ) is open by TOPS_1: 3;

      then

       A4: (A ` ) = ( union { G where G be Subset of T : G in BB & G c= (A ` ) }) by YELLOW_8: 9;

      set F = { (f " G) where G be Subset of T : G in BB & G c= (A ` ) };

      F c= ( bool the carrier of S)

      proof

        let a be object;

        assume a in F;

        then ex G be Subset of T st a = (f " G) & G in BB & G c= (A ` );

        hence thesis;

      end;

      then

      reconsider F as Subset-Family of S;

      reconsider F as Subset-Family of S;

      F c= the topology of S

      proof

        let a be object;

        assume a in F;

        then

        consider G be Subset of T such that

         A5: a = (f " G) and

         A6: G in BB and G c= (A ` );

        

         A7: (f " (G ` )) is closed by A3, A6;

        ((f " G) ` ) = (f " (G ` )) by Th2;

        then (f " G) is open by A7, TOPS_1: 4;

        hence thesis by A5;

      end;

      then

       A8: ( union F) in the topology of S by PRE_TOPC:def 1;

      defpred P[ Subset of T] means $1 in BB & $1 c= (A ` );

      deffunc F( Subset of T) = $1;

      (f " ( union { F(G) where G be Subset of T : P[G] })) = ( union { (f " F(G)) where G be Subset of T : P[G] }) from ABC;

      then (f " (A ` )) is open by A4, A8;

      then ((f " A) ` ) is open by Th2;

      hence thesis by TOPS_1: 3;

    end;

    theorem :: YELLOW_9:34

    for S be TopSpace, T be non empty TopSpace, K be Basis of T holds for f be Function of S, T holds f is continuous iff for A be Subset of T st A in K holds (f " A) is open

    proof

      let S be TopSpace, T be non empty TopSpace, K be Basis of T;

      let f be Function of S, T;

      hereby

        assume

         A1: f is continuous;

        let A be Subset of T;

        assume A in K;

        then (f " (A ` )) is closed by A1, Th33;

        then ((f " A) ` ) is closed by Th2;

        hence (f " A) is open by TOPS_1: 4;

      end;

      assume

       A2: for A be Subset of T st A in K holds (f " A) is open;

      now

        let A be Subset of T;

        assume A in K;

        then (f " A) is open by A2;

        then ((f " A) ` ) is closed by TOPS_1: 4;

        hence (f " (A ` )) is closed by Th2;

      end;

      hence thesis by Th33;

    end;

    theorem :: YELLOW_9:35

    

     Th35: for S be TopSpace, T be non empty TopSpace, K be prebasis of T holds for f be Function of S, T holds f is continuous iff for A be Subset of T st A in K holds (f " (A ` )) is closed

    proof

      let S be TopSpace, T be non empty TopSpace, BB be prebasis of T, f be Function of S, T;

      

       A1: BB c= the topology of T by TOPS_2: 64;

      hereby

        assume

         A2: f is continuous;

        let A be Subset of T;

        assume A in BB;

        then A is open by A1;

        then (A ` ) is closed by TOPS_1: 4;

        hence (f " (A ` )) is closed by A2;

      end;

      assume

       A3: for A be Subset of T st A in BB holds (f " (A ` )) is closed;

      reconsider C = ( FinMeetCl BB) as Basis of T by Th23;

      now

        let A be Subset of T;

        assume A in C;

        then

        consider Y be Subset-Family of T such that

         A4: Y c= BB and

         A5: Y is finite and

         A6: A = ( Intersect Y) by CANTOR_1:def 3;

        reconsider Y as Subset-Family of T;

        reconsider CY = ( COMPLEMENT Y) as Subset-Family of T;

        defpred P[ set] means $1 in Y;

        deffunc F( Subset of T) = ($1 ` );

        

         A7: (f " (A ` )) = (f " ( union CY)) by A6, YELLOW_8: 7

        .= (f " ( union { F(a) where a be Subset of T : P[a] })) by Th3

        .= ( union { (f " F(y)) where y be Subset of T : P[y] }) from ABC;

        set X = { (f " (y ` )) where y be Subset of T : y in Y };

        X c= ( bool the carrier of S)

        proof

          let x be object;

          assume x in X;

          then ex y be Subset of T st x = (f " (y ` )) & y in Y;

          hence thesis;

        end;

        then

        reconsider X as Subset-Family of S;

        reconsider X as Subset-Family of S;

        

         A8: X is closed

        proof

          let a be Subset of S;

          assume a in X;

          then ex y be Subset of T st a = (f " (y ` )) & y in Y;

          hence thesis by A3, A4;

        end;

        

         A9: Y is finite by A5;

        deffunc F( Subset of T) = (f " ($1 ` ));

        { F(y) where y be Subset of T : y in Y } is finite from FRAENKEL:sch 21( A9);

        hence (f " (A ` )) is closed by A7, A8, TOPS_2: 21;

      end;

      hence thesis by Th33;

    end;

    theorem :: YELLOW_9:36

    for S be TopSpace, T be non empty TopSpace, K be prebasis of T holds for f be Function of S, T holds f is continuous iff for A be Subset of T st A in K holds (f " A) is open

    proof

      let S be TopSpace, T be non empty TopSpace, K be prebasis of T;

      let f be Function of S, T;

      hereby

        assume

         A1: f is continuous;

        let A be Subset of T;

        assume A in K;

        then (f " (A ` )) is closed by A1, Th35;

        then ((f " A) ` ) is closed by Th2;

        hence (f " A) is open by TOPS_1: 4;

      end;

      assume

       A2: for A be Subset of T st A in K holds (f " A) is open;

      now

        let A be Subset of T;

        assume A in K;

        then (f " A) is open by A2;

        then ((f " A) ` ) is closed by TOPS_1: 4;

        hence (f " (A ` )) is closed by Th2;

      end;

      hence thesis by Th35;

    end;

    theorem :: YELLOW_9:37

    

     Th37: for T be non empty TopSpace, x be Point of T, X be Subset of T holds for K be Basis of T st for A be Subset of T st A in K & x in A holds A meets X holds x in ( Cl X)

    proof

      let T be non empty TopSpace, x be Point of T, X be Subset of T;

      let BB be Basis of T such that

       A1: for A be Subset of T st A in BB & x in A holds A meets X;

      now

        let G be a_neighborhood of x;

        

         A2: ( Int G) = ( union { A where A be Subset of T : A in BB & A c= G }) by YELLOW_8: 11;

        x in ( Int G) by CONNSP_2:def 1;

        then

        consider Z be set such that

         A3: x in Z and

         A4: Z in { A where A be Subset of T : A in BB & A c= G } by A2, TARSKI:def 4;

        ex A be Subset of T st (Z = A) & (A in BB) & (A c= G) by A4;

        hence G meets X by A1, A3, XBOOLE_1: 63;

      end;

      hence thesis by CONNSP_2: 27;

    end;

    theorem :: YELLOW_9:38

    

     Th38: for T be non empty TopSpace, x be Point of T, X be Subset of T holds for K be prebasis of T st for Z be finite Subset-Family of T st Z c= K & x in ( Intersect Z) holds ( Intersect Z) meets X holds x in ( Cl X)

    proof

      let T be non empty TopSpace, x be Point of T, X be Subset of T;

      let BB be prebasis of T such that

       A1: for Z be finite Subset-Family of T st Z c= BB & x in ( Intersect Z) holds ( Intersect Z) meets X;

      reconsider BB9 = ( FinMeetCl BB) as Basis of T by Th23;

      now

        let A be Subset of T;

        assume A in BB9;

        then

         A2: ex Y be Subset-Family of T st (Y c= BB) & (Y is finite) & (A = ( Intersect Y)) by CANTOR_1:def 3;

        assume x in A;

        hence A meets X by A1, A2;

      end;

      hence thesis by Th37;

    end;

    theorem :: YELLOW_9:39

    for T be non empty TopSpace, K be prebasis of T, x be Point of T holds for N be net of T st for A be Subset of T st A in K & x in A holds N is_eventually_in A holds for S be Subset of T st ( rng ( netmap (N,T))) c= S holds x in ( Cl S)

    proof

      let T be non empty TopSpace, BB be prebasis of T, x be Point of T, N be net of T such that

       A1: for A be Subset of T st A in BB & x in A holds N is_eventually_in A;

      let S be Subset of T such that

       A2: ( rng ( netmap (N,T))) c= S;

      

       A3: ( [#] N) is directed by WAYBEL_0:def 6;

      now

        let Z be finite Subset-Family of T;

        assume that

         A4: Z c= BB and

         A5: x in ( Intersect Z);

        defpred P[ object, object] means for i,j be Element of N st $2 = i & i <= j holds ex pp be set st pp = $1 & (N . j) in pp;

         A6:

        now

          let a be object;

          assume

           A7: a in Z;

          then

          reconsider A = a as Subset of T;

          x in A by A5, A7, SETFAM_1: 43;

          then N is_eventually_in A by A1, A4, A7;

          then

          consider i be Element of N such that

           A8: for j be Element of N st i <= j holds (N . j) in A;

          reconsider b = i as object;

          take b;

          thus b in the carrier of N & P[a, b] by A8;

        end;

        consider f be Function such that

         A9: ( dom f) = Z & ( rng f) c= the carrier of N & for a be object st a in Z holds P[a, (f . a)] from FUNCT_1:sch 6( A6);

        set k = the Element of N;

        per cases by A9, RELAT_1: 42;

          suppose Z = {} ;

          then

           A10: ( Intersect Z) = the carrier of T by SETFAM_1:def 9;

          (N . k) in ( rng ( netmap (N,T))) by FUNCT_2: 4;

          hence ( Intersect Z) meets S by A2, A10, XBOOLE_0: 3;

        end;

          suppose ( rng f) <> {} ;

          then

          reconsider Y = ( rng f) as finite non empty Subset of N by A9, FINSET_1: 8;

          consider i be Element of N such that i in the carrier of N and

           A11: i is_>=_than Y by A3, WAYBEL_0: 1;

          now

            let y be set;

            assume

             A12: y in Z;

            then

             A13: (f . y) in Y by A9, FUNCT_1:def 3;

            then

            reconsider j = (f . y) as Element of N;

            

             A14: j <= i by A11, A13, LATTICE3:def 9;

             P[y, j] by A9, A12;

            then ex pp be set st pp = y & (N . i) in pp by A14;

            hence (N . i) in y;

          end;

          then

           A15: (N . i) in ( Intersect Z) by SETFAM_1: 43;

          (N . i) in ( rng ( netmap (N,T))) by FUNCT_2: 4;

          hence ( Intersect Z) meets S by A2, A15, XBOOLE_0: 3;

        end;

      end;

      hence thesis by Th38;

    end;

    begin

    theorem :: YELLOW_9:40

    

     Th40: for T1,T2 be non empty TopSpace holds for B1 be Basis of T1, B2 be Basis of T2 holds { [:a, b:] where a be Subset of T1, b be Subset of T2 : a in B1 & b in B2 } is Basis of [:T1, T2:]

    proof

      let T1,T2 be non empty TopSpace;

      let B1 be Basis of T1, B2 be Basis of T2;

      set BB = { [:a, b:] where a be Subset of T1, b be Subset of T2 : a in B1 & b in B2 };

      set T = [:T1, T2:];

      

       A1: the carrier of T = [:the carrier of T1, the carrier of T2:] by BORSUK_1:def 2;

      BB c= ( bool the carrier of T)

      proof

        let x be object;

        assume x in BB;

        then ex a be Subset of T1, b be Subset of T2 st x = [:a, b:] & a in B1 & b in B2;

        hence thesis;

      end;

      then

      reconsider BB as Subset-Family of T;

      

       A2: B1 c= the topology of T1 by TOPS_2: 64;

      

       A3: B2 c= the topology of T2 by TOPS_2: 64;

      BB is Basis of T

      proof

        

         A4: BB is open

        proof

          let x be Subset of T;

          assume x in BB;

          then

          consider a be Subset of T1, b be Subset of T2 such that

           A5: x = [:a, b:] and

           A6: a in B1 and

           A7: b in B2;

          

           A8: a is open by A2, A6;

          b is open by A3, A7;

          hence x is open by A5, A8, BORSUK_1: 6;

        end;

        BB is quasi_basis

        proof

          let x be object;

          assume

           A9: x in the topology of T;

          then

          reconsider X = x as Subset of T;

          X is open by A9;

          then

           A10: X = ( union ( Base-Appr X)) by BORSUK_1: 13;

          set Y = (BB /\ ( Base-Appr X));

          

           A11: Y c= BB by XBOOLE_1: 17;

          reconsider Y as Subset-Family of T;

          ( union Y) = X

          proof

            thus ( union Y) c= X by A10, XBOOLE_1: 17, ZFMISC_1: 77;

            let z be object;

            assume

             A12: z in X;

            then

            reconsider p = z as Point of T;

            consider z1,z2 be object such that

             A13: z1 in the carrier of T1 and

             A14: z2 in the carrier of T2 and

             A15: p = [z1, z2] by A1, ZFMISC_1:def 2;

            reconsider z1 as Point of T1 by A13;

            reconsider z2 as Point of T2 by A14;

            consider Z be set such that

             A16: z in Z and

             A17: Z in ( Base-Appr X) by A10, A12, TARSKI:def 4;

            

             A18: ( Base-Appr X) = { [:a, b:] where a be Subset of T1, b be Subset of T2 : [:a, b:] c= X & a is open & b is open } by BORSUK_1:def 3;

            then

            consider a be Subset of T1, b be Subset of T2 such that

             A19: Z = [:a, b:] and

             A20: [:a, b:] c= X and

             A21: a is open and

             A22: b is open by A17;

            

             A23: z1 in a by A15, A16, A19, ZFMISC_1: 87;

            

             A24: z2 in b by A15, A16, A19, ZFMISC_1: 87;

            consider a9 be Subset of T1 such that

             A25: a9 in B1 and

             A26: z1 in a9 and

             A27: a9 c= a by A21, A23, Th31;

            consider b9 be Subset of T2 such that

             A28: b9 in B2 and

             A29: z2 in b9 and

             A30: b9 c= b by A22, A24, Th31;

             [:a9, b9:] c= [:a, b:] by A27, A30, ZFMISC_1: 96;

            then

             A31: [:a9, b9:] c= X by A20;

            

             A32: a9 is open by A2, A25;

            b9 is open by A3, A28;

            then

             A33: [:a9, b9:] in ( Base-Appr X) by A18, A31, A32;

            

             A34: [:a9, b9:] in BB by A25, A28;

            

             A35: p in [:a9, b9:] by A15, A26, A29, ZFMISC_1: 87;

             [:a9, b9:] in Y by A33, A34, XBOOLE_0:def 4;

            hence thesis by A35, TARSKI:def 4;

          end;

          hence thesis by A11, CANTOR_1:def 1;

        end;

        hence thesis by A4;

      end;

      hence thesis;

    end;

    theorem :: YELLOW_9:41

    

     Th41: for T1,T2 be non empty TopSpace holds for B1 be prebasis of T1, B2 be prebasis of T2 holds ({ [:the carrier of T1, b:] where b be Subset of T2 : b in B2 } \/ { [:a, the carrier of T2:] where a be Subset of T1 : a in B1 }) is prebasis of [:T1, T2:]

    proof

      let T1,T2 be non empty TopSpace;

      set T = [:T1, T2:];

      let B1 be prebasis of T1, B2 be prebasis of T2;

      set C2 = { [:the carrier of T1, b:] where b be Subset of T2 : b in B2 };

      set C1 = { [:a, the carrier of T2:] where a be Subset of T1 : a in B1 };

      reconsider D1 = ( FinMeetCl B1) as Basis of T1 by Th23;

      reconsider D2 = ( FinMeetCl B2) as Basis of T2 by Th23;

      reconsider D = { [:a, b:] where a be Subset of T1, b be Subset of T2 : a in D1 & b in D2 } as Basis of T by Th40;

      the carrier of T1 c= the carrier of T1;

      then

      reconsider cT1 = the carrier of T1 as Subset of T1;

      the carrier of T2 c= the carrier of T2;

      then

      reconsider cT2 = the carrier of T2 as Subset of T2;

      

       A1: cT1 in the topology of T1 by PRE_TOPC:def 1;

      

       A2: cT2 in the topology of T2 by PRE_TOPC:def 1;

      

       A3: B1 c= the topology of T1 by TOPS_2: 64;

      

       A4: B2 c= the topology of T2 by TOPS_2: 64;

      C1 c= ( bool the carrier of T)

      proof

        let x be object;

        assume x in C1;

        then ex a be Subset of T1 st x = [:a, cT2:] & a in B1;

        hence thesis;

      end;

      then

      reconsider C1 as Subset-Family of T;

      reconsider C1 as Subset-Family of T;

      C2 c= ( bool the carrier of T)

      proof

        let x be object;

        assume x in C2;

        then ex a be Subset of T2 st x = [:cT1, a:] & a in B2;

        hence thesis;

      end;

      then

      reconsider C2 as Subset-Family of T;

      reconsider C2 as Subset-Family of T;

      reconsider C = (C2 \/ C1) as Subset-Family of T;

      C is prebasis of T

      proof

        

         A5: C is open

        proof

          let x be Subset of T;

          assume x in C;

          then x in C1 or x in C2 by XBOOLE_0:def 3;

          then (ex a be Subset of T1 st x = [:a, cT2:] & a in B1) or ex a be Subset of T2 st x = [:cT1, a:] & a in B2;

          then

          consider a be Subset of T1, b be Subset of T2 such that

           A6: x = [:a, b:] and

           A7: a in the topology of T1 and

           A8: b in the topology of T2 by A1, A2, A3, A4;

          

           A9: a is open by A7;

          b is open by A8;

          hence x is open by A6, A9, BORSUK_1: 6;

        end;

        C is quasi_prebasis

        proof

          take D;

          let d be object;

          assume d in D;

          then

          consider a be Subset of T1, b be Subset of T2 such that

           A10: d = [:a, b:] and

           A11: a in D1 and

           A12: b in D2;

          consider aY be Subset-Family of T1 such that

           A13: aY c= B1 and

           A14: aY is finite and

           A15: a = ( Intersect aY) by A11, CANTOR_1:def 3;

          consider bY be Subset-Family of T2 such that

           A16: bY c= B2 and

           A17: bY is finite and

           A18: b = ( Intersect bY) by A12, CANTOR_1:def 3;

          deffunc F( Subset of T1) = [:$1, cT2:];

          

           A19: { F(s) where s be Subset of T1 : s in aY } is finite from FRAENKEL:sch 21( A14);

          deffunc G( Subset of T2) = [:cT1, $1:];

          

           A20: { G(s) where s be Subset of T2 : s in bY } is finite from FRAENKEL:sch 21( A17);

          set Y1 = { [:s, cT2:] where s be Subset of T1 : s in aY };

          set Y2 = { [:cT1, s:] where s be Subset of T2 : s in bY };

          

           A21: Y1 c= C

          proof

            let x be object;

            assume x in Y1;

            then ex s be Subset of T1 st (x = [:s, cT2:]) & (s in aY);

            then x in C1 by A13;

            hence thesis by XBOOLE_0:def 3;

          end;

          

           A22: Y2 c= C

          proof

            let x be object;

            assume x in Y2;

            then ex s be Subset of T2 st (x = [:cT1, s:]) & (s in bY);

            then x in C2 by A16;

            hence thesis by XBOOLE_0:def 3;

          end;

          set Y = (Y1 \/ Y2);

          

           A23: Y c= C by A21, A22, XBOOLE_1: 8;

          then

          reconsider Y as Subset-Family of T by XBOOLE_1: 1;

          ( Intersect Y) = [:a, b:]

          proof

            hereby

              let p be object;

              assume

               A24: p in ( Intersect Y);

              then

              consider p1 be Point of T1, p2 be Point of T2 such that

               A25: p = [p1, p2] by BORSUK_1: 10;

              now

                let z be set;

                assume

                 A26: z in aY;

                then

                reconsider z9 = z as Subset of T1;

                 [:z9, cT2:] in Y1 by A26;

                then [:z9, cT2:] in Y by XBOOLE_0:def 3;

                then p in [:z9, cT2:] by A24, SETFAM_1: 43;

                hence p1 in z by A25, ZFMISC_1: 87;

              end;

              then

               A27: p1 in a by A15, SETFAM_1: 43;

              now

                let z be set;

                assume

                 A28: z in bY;

                then

                reconsider z9 = z as Subset of T2;

                 [:cT1, z9:] in Y2 by A28;

                then [:cT1, z9:] in Y by XBOOLE_0:def 3;

                then p in [:cT1, z9:] by A24, SETFAM_1: 43;

                hence p2 in z by A25, ZFMISC_1: 87;

              end;

              then p2 in b by A18, SETFAM_1: 43;

              hence p in [:a, b:] by A25, A27, ZFMISC_1: 87;

            end;

            let p be object;

            assume p in [:a, b:];

            then

            consider p1,p2 be object such that

             A29: p1 in a and

             A30: p2 in b and

             A31: [p1, p2] = p by ZFMISC_1:def 2;

            reconsider p1 as Point of T1 by A29;

            reconsider p2 as Point of T2 by A30;

            now

              let z be set;

              assume

               A32: z in Y;

              per cases by A32, XBOOLE_0:def 3;

                suppose z in Y1;

                then

                consider s be Subset of T1 such that

                 A33: z = [:s, cT2:] and

                 A34: s in aY;

                p1 in s by A15, A29, A34, SETFAM_1: 43;

                hence [p1, p2] in z by A33, ZFMISC_1: 87;

              end;

                suppose z in Y2;

                then

                consider s be Subset of T2 such that

                 A35: z = [:cT1, s:] and

                 A36: s in bY;

                p2 in s by A18, A30, A36, SETFAM_1: 43;

                hence [p1, p2] in z by A35, ZFMISC_1: 87;

              end;

            end;

            hence thesis by A31, SETFAM_1: 43;

          end;

          hence thesis by A19, A20, A23, CANTOR_1:def 3, A10;

        end;

        hence thesis by A5;

      end;

      hence thesis;

    end;

    theorem :: YELLOW_9:42

    for X1,X2 be set, A be Subset-Family of [:X1, X2:] holds for A1 be non empty Subset-Family of X1 holds for A2 be non empty Subset-Family of X2 st A = { [:a, b:] where a be Subset of X1, b be Subset of X2 : a in A1 & b in A2 } holds ( Intersect A) = [:( Intersect A1), ( Intersect A2):]

    proof

      let X1,X2 be set, A be Subset-Family of [:X1, X2:];

      let A1 be non empty Subset-Family of X1, A2 be non empty Subset-Family of X2 such that

       A1: A = { [:a, b:] where a be Subset of X1, b be Subset of X2 : a in A1 & b in A2 };

      hereby

        let x be object;

        assume

         A2: x in ( Intersect A);

        then

        consider x1,x2 be object such that

         A3: x1 in X1 and

         A4: x2 in X2 and

         A5: [x1, x2] = x by ZFMISC_1:def 2;

        set a1 = the Element of A1, a2 = the Element of A2;

        reconsider a1 as Subset of X1;

        reconsider a2 as Subset of X2;

        now

          let a be set;

          assume a in A1;

          then [:a, a2:] in A by A1;

          then x in [:a, a2:] by A2, SETFAM_1: 43;

          hence x1 in a by A5, ZFMISC_1: 87;

        end;

        then

         A6: x1 in ( Intersect A1) by A3, SETFAM_1: 43;

        now

          let a be set;

          assume a in A2;

          then [:a1, a:] in A by A1;

          then x in [:a1, a:] by A2, SETFAM_1: 43;

          hence x2 in a by A5, ZFMISC_1: 87;

        end;

        then x2 in ( Intersect A2) by A4, SETFAM_1: 43;

        hence x in [:( Intersect A1), ( Intersect A2):] by A5, A6, ZFMISC_1: 87;

      end;

      let x be object;

      assume

       A7: x in [:( Intersect A1), ( Intersect A2):];

      then

      consider x1,x2 be object such that

       A8: x1 in ( Intersect A1) and

       A9: x2 in ( Intersect A2) and

       A10: [x1, x2] = x by ZFMISC_1:def 2;

      now

        let c be set;

        assume c in A;

        then

        consider a be Subset of X1, b be Subset of X2 such that

         A11: c = [:a, b:] and

         A12: a in A1 and

         A13: b in A2 by A1;

        

         A14: x1 in a by A8, A12, SETFAM_1: 43;

        x2 in b by A9, A13, SETFAM_1: 43;

        hence x in c by A10, A11, A14, ZFMISC_1: 87;

      end;

      hence thesis by A7, SETFAM_1: 43;

    end;

    theorem :: YELLOW_9:43

    for T1,T2 be non empty TopSpace holds for B1 be prebasis of T1, B2 be prebasis of T2 st ( union B1) = the carrier of T1 & ( union B2) = the carrier of T2 holds { [:a, b:] where a be Subset of T1, b be Subset of T2 : a in B1 & b in B2 } is prebasis of [:T1, T2:]

    proof

      let T1,T2 be non empty TopSpace;

      let B1 be prebasis of T1, B2 be prebasis of T2 such that

       A1: ( union B1) = the carrier of T1 and

       A2: ( union B2) = the carrier of T2;

      set cT1 = the carrier of T1, cT2 = the carrier of T2;

      set BB1 = { [:the carrier of T1, b:] where b be Subset of T2 : b in B2 }, BB2 = { [:a, the carrier of T2:] where a be Subset of T1 : a in B1 };

      set CC = { [:a, b:] where a be Subset of T1, b be Subset of T2 : a in B1 & b in B2 };

      set T = [:T1, T2:];

      reconsider BB = (BB1 \/ BB2) as prebasis of [:T1, T2:] by Th41;

      

       A3: ( FinMeetCl BB) is Basis of T by Th23;

      CC c= ( bool the carrier of [:T1, T2:])

      proof

        let x be object;

        assume x in CC;

        then ex a be Subset of T1, b be Subset of T2 st x = [:a, b:] & a in B1 & b in B2;

        hence thesis;

      end;

      then

      reconsider CC as Subset-Family of [:T1, T2:];

      reconsider CC as Subset-Family of [:T1, T2:];

      CC c= the topology of T

      proof

        let x be object;

        assume x in CC;

        then

        consider a be Subset of T1, b be Subset of T2 such that

         A4: x = [:a, b:] and

         A5: a in B1 and

         A6: b in B2;

        

         A7: B1 c= the topology of T1 by TOPS_2: 64;

        

         A8: B2 c= the topology of T2 by TOPS_2: 64;

        

         A9: a is open by A5, A7;

        b is open by A6, A8;

        then [:a, b:] is open by A9, BORSUK_1: 6;

        hence thesis by A4;

      end;

      then ( UniCl CC) c= ( UniCl the topology of T) by CANTOR_1: 9;

      then

       A10: ( UniCl CC) c= the topology of T by CANTOR_1: 6;

      BB c= ( UniCl CC)

      proof

        let x be object;

        assume

         A11: x in BB;

        per cases by A11, XBOOLE_0:def 3;

          suppose x in BB1;

          then

          consider b be Subset of T2 such that

           A12: x = [:cT1, b:] and

           A13: b in B2;

          set Y = { [:a, b:] where a be Subset of T1 : a in B1 };

          Y c= ( bool the carrier of T)

          proof

            let y be object;

            assume y in Y;

            then ex a be Subset of T1 st y = [:a, b:] & a in B1;

            hence thesis;

          end;

          then

          reconsider Y as Subset-Family of T;

          reconsider Y as Subset-Family of T;

          

           A14: Y c= CC

          proof

            let y be object;

            assume y in Y;

            then ex a be Subset of T1 st y = [:a, b:] & a in B1;

            hence thesis by A13;

          end;

           [:cT1, b:] = ( union Y)

          proof

            hereby

              let z be object;

              assume z in [:cT1, b:];

              then

              consider p1,p2 be object such that

               A15: p1 in cT1 and

               A16: p2 in b and

               A17: [p1, p2] = z by ZFMISC_1:def 2;

              consider a be set such that

               A18: p1 in a and

               A19: a in B1 by A1, A15, TARSKI:def 4;

              reconsider a as Subset of T1 by A19;

              

               A20: [:a, b:] in Y by A19;

              z in [:a, b:] by A16, A17, A18, ZFMISC_1:def 2;

              hence z in ( union Y) by A20, TARSKI:def 4;

            end;

            let z be object;

            assume z in ( union Y);

            then

            consider y be set such that

             A21: z in y and

             A22: y in Y by TARSKI:def 4;

            ex a be Subset of T1 st y = [:a, b:] & a in B1 by A22;

            then y c= [:cT1, b:] by ZFMISC_1: 95;

            hence thesis by A21;

          end;

          hence thesis by A14, CANTOR_1:def 1, A12;

        end;

          suppose x in BB2;

          then

          consider a be Subset of T1 such that

           A23: x = [:a, cT2:] and

           A24: a in B1;

          set Y = { [:a, b:] where b be Subset of T2 : b in B2 };

          Y c= ( bool the carrier of T)

          proof

            let y be object;

            assume y in Y;

            then ex b be Subset of T2 st y = [:a, b:] & b in B2;

            hence thesis;

          end;

          then

          reconsider Y as Subset-Family of T;

          reconsider Y as Subset-Family of T;

          

           A25: Y c= CC

          proof

            let y be object;

            assume y in Y;

            then ex b be Subset of T2 st y = [:a, b:] & b in B2;

            hence thesis by A24;

          end;

           [:a, cT2:] = ( union Y)

          proof

            hereby

              let z be object;

              assume z in [:a, cT2:];

              then

              consider p1,p2 be object such that

               A26: p1 in a and

               A27: p2 in cT2 and

               A28: [p1, p2] = z by ZFMISC_1:def 2;

              consider b be set such that

               A29: p2 in b and

               A30: b in B2 by A2, A27, TARSKI:def 4;

              reconsider b as Subset of T2 by A30;

              

               A31: [:a, b:] in Y by A30;

              z in [:a, b:] by A26, A28, A29, ZFMISC_1:def 2;

              hence z in ( union Y) by A31, TARSKI:def 4;

            end;

            let z be object;

            assume z in ( union Y);

            then

            consider y be set such that

             A32: z in y and

             A33: y in Y by TARSKI:def 4;

            ex b be Subset of T2 st y = [:a, b:] & b in B2 by A33;

            then y c= [:a, cT2:] by ZFMISC_1: 95;

            hence thesis by A32;

          end;

          hence thesis by A25, CANTOR_1:def 1, A23;

        end;

      end;

      then ( FinMeetCl BB) c= ( FinMeetCl ( UniCl CC)) by CANTOR_1: 14;

      then ( UniCl CC) is prebasis of T by A3, A10, CANTOR_1:def 4, TOPS_2: 64;

      hence thesis by Th24;

    end;

    begin

    definition

      let R be RelStr;

      :: YELLOW_9:def4

      mode TopAugmentation of R -> TopRelStr means

      : Def4: the RelStr of it = the RelStr of R;

      existence

      proof

        take TopRelStr (# the carrier of R, the InternalRel of R, ( {} ( bool the carrier of R)) #);

        thus thesis;

      end;

    end

    notation

      let R be RelStr;

      let T be TopAugmentation of R;

      synonym T is correct for T is TopSpace-like;

    end

    registration

      let R be RelStr;

      cluster correct discrete strict for TopAugmentation of R;

      existence

      proof

        reconsider BB = ( bool the carrier of R) as Subset-Family of R;

        set T = TopRelStr (# the carrier of R, the InternalRel of R, BB #);

         the RelStr of R = the RelStr of T;

        then

        reconsider T as TopAugmentation of R by Def4;

        take T;

        T is discrete TopStruct by TDLAT_3:def 1;

        hence thesis;

      end;

    end

    theorem :: YELLOW_9:44

    for T be TopRelStr holds T is TopAugmentation of T

    proof

      let T be TopRelStr;

      thus the RelStr of T = the RelStr of T;

    end;

    theorem :: YELLOW_9:45

    for S be TopRelStr, T be TopAugmentation of S holds S is TopAugmentation of T

    proof

      let S be TopRelStr, T be TopAugmentation of S;

      thus the RelStr of S = the RelStr of T by Def4;

    end;

    theorem :: YELLOW_9:46

    for R be RelStr, T1 be TopAugmentation of R holds for T2 be TopAugmentation of T1 holds T2 is TopAugmentation of R

    proof

      let R be RelStr, T1 be TopAugmentation of R;

      let T2 be TopAugmentation of T1;

      

      thus the RelStr of T2 = the RelStr of T1 by Def4

      .= the RelStr of R by Def4;

    end;

    registration

      let R be non empty RelStr;

      cluster -> non empty for TopAugmentation of R;

      coherence

      proof

        let T be TopAugmentation of R;

         the RelStr of T = the RelStr of R by Def4;

        hence the carrier of T is non empty;

      end;

    end

    registration

      let R be reflexive RelStr;

      cluster -> reflexive for TopAugmentation of R;

      coherence

      proof

        let T be TopAugmentation of R;

         the RelStr of T = the RelStr of R by Def4;

        hence the InternalRel of T is_reflexive_in the carrier of T by ORDERS_2:def 2;

      end;

    end

    registration

      let R be transitive RelStr;

      cluster -> transitive for TopAugmentation of R;

      coherence

      proof

        let T be TopAugmentation of R;

         the RelStr of T = the RelStr of R by Def4;

        then the InternalRel of T is_transitive_in the carrier of T by ORDERS_2:def 3;

        hence thesis;

      end;

    end

    registration

      let R be antisymmetric RelStr;

      cluster -> antisymmetric for TopAugmentation of R;

      coherence

      proof

        let T be TopAugmentation of R;

         the RelStr of T = the RelStr of R by Def4;

        then the InternalRel of T is_antisymmetric_in the carrier of T by ORDERS_2:def 4;

        hence thesis;

      end;

    end

    registration

      let R be complete non empty RelStr;

      cluster -> complete for TopAugmentation of R;

      coherence

      proof

        let T be TopAugmentation of R;

         the RelStr of T = the RelStr of R by Def4;

        hence thesis by YELLOW_0: 3;

      end;

    end

    theorem :: YELLOW_9:47

    

     Th47: for S be up-complete antisymmetric non empty reflexive RelStr, T be non empty reflexive RelStr st the RelStr of S = the RelStr of T holds for A be Subset of S, C be Subset of T st A = C & A is inaccessible holds C is inaccessible

    proof

      let S be up-complete antisymmetric non empty reflexive RelStr, T be non empty reflexive RelStr such that

       A1: the RelStr of S = the RelStr of T;

      let A be Subset of S, C be Subset of T such that

       A2: A = C and

       A3: for D be non empty directed Subset of S st ( sup D) in A holds D meets A;

      let D be non empty directed Subset of T such that

       A4: ( sup D) in C;

      reconsider E = D as non empty directed Subset of S by A1, WAYBEL_0: 3;

       ex_sup_of (E,S) by WAYBEL_0: 75;

      then ( sup D) = ( sup E) by A1, YELLOW_0: 26;

      hence thesis by A2, A3, A4;

    end;

    theorem :: YELLOW_9:48

    

     Th48: for S be non empty reflexive RelStr, T be TopAugmentation of S st the topology of T = ( sigma S) holds T is correct

    proof

      let R be non empty reflexive RelStr;

      let T be TopAugmentation of R such that

       A1: the topology of T = ( sigma R);

      

       A2: the RelStr of T = the RelStr of R by Def4;

      set IT = ( ConvergenceSpace ( Scott-Convergence R));

      

       A3: the carrier of IT = the carrier of R by YELLOW_6:def 24;

      then

       A4: the carrier of T in ( sigma R) by A2, PRE_TOPC:def 1;

      

       A5: for a be Subset-Family of T st a c= the topology of T holds ( union a) in the topology of T by A1, A2, A3, PRE_TOPC:def 1;

      for a,b be Subset of T st a in the topology of T & b in the topology of T holds (a /\ b) in the topology of T by A1, PRE_TOPC:def 1;

      hence thesis by A1, A4, A5;

    end;

    theorem :: YELLOW_9:49

    

     Th49: for S be complete LATTICE, T be TopAugmentation of S st the topology of T = ( sigma S) holds T is Scott

    proof

      let R be complete LATTICE;

      let T be TopAugmentation of R such that

       A1: the topology of T = ( sigma R);

      

       A2: the RelStr of T = the RelStr of R by Def4;

      T is Scott

      proof

        let S be Subset of T;

        reconsider A = S as Subset of R by A2;

        thus S is open implies S is inaccessible upper by A1, WAYBEL11: 31, A2, Th47, WAYBEL_0: 25;

        assume S is inaccessible upper;

        then A is inaccessible upper by A2, Th47, WAYBEL_0: 25;

        hence S in the topology of T by A1, WAYBEL11: 31;

      end;

      hence thesis;

    end;

    registration

      let R be complete LATTICE;

      cluster Scott strict correct for TopAugmentation of R;

      existence

      proof

        set T = TopRelStr (# the carrier of R, the InternalRel of R, ( sigma R) #);

         the RelStr of T = the RelStr of R;

        then

        reconsider T as TopAugmentation of R by Def4;

        take T;

        thus thesis by Th48, Th49;

      end;

    end

    theorem :: YELLOW_9:50

    

     Th50: for S,T be complete Scott non empty reflexive transitive antisymmetric TopRelStr st the RelStr of S = the RelStr of T holds for F be Subset of S, G be Subset of T st F = G holds F is open implies G is open

    proof

      let S,T be complete Scott non empty reflexive transitive antisymmetric TopRelStr such that

       A1: the RelStr of S = the RelStr of T;

      let F be Subset of S, G be Subset of T;

      assume that

       A2: F = G and

       A3: F is open;

      F is upper inaccessible by A3, WAYBEL11:def 4;

      then G is upper inaccessible by A1, A2, Th47, WAYBEL_0: 25;

      hence thesis by WAYBEL11:def 4;

    end;

    theorem :: YELLOW_9:51

    

     Th51: for S be complete LATTICE, T be Scott TopAugmentation of S holds the topology of T = ( sigma S)

    proof

      let S be complete LATTICE;

      let T be Scott TopAugmentation of S;

      set R = TopRelStr (# the carrier of S, the InternalRel of S, ( sigma S) #);

       the RelStr of R = the RelStr of S;

      then

      reconsider R as TopAugmentation of S by Def4;

      reconsider R as correct Scott TopAugmentation of S by Th48, Th49;

      

       A1: the RelStr of T = the RelStr of R by Def4;

      thus the topology of T c= ( sigma S)

      proof

        let x be object;

        assume

         A2: x in the topology of T;

        then

        reconsider A = x as Subset of T;

        reconsider C = A as Subset of R by A1;

        A is open by A2;

        then C is open by A1, Th50;

        hence thesis;

      end;

      let x be object;

      assume

       A3: x in ( sigma S);

      then

      reconsider A = x as Subset of R;

      reconsider C = A as Subset of T by A1;

      A is open by A3;

      then C is open by A1, Th50;

      hence thesis;

    end;

    theorem :: YELLOW_9:52

    for S,T be complete LATTICE st the RelStr of S = the RelStr of T holds ( sigma S) = ( sigma T)

    proof

      let S,T be complete LATTICE such that

       A1: the RelStr of S = the RelStr of T;

      set A = the Scott correct TopAugmentation of S;

       the RelStr of A = the RelStr of S by Def4;

      then A is Scott correct TopAugmentation of T by A1, Def4;

      then the topology of A = ( sigma T) by Th51;

      hence thesis by Th51;

    end;

    registration

      let R be complete LATTICE;

      cluster Scott -> correct for TopAugmentation of R;

      coherence

      proof

        let T be TopAugmentation of R;

        assume T is Scott;

        then the topology of T = ( sigma R) by Th51;

        hence thesis by Th48;

      end;

    end

    

     Lm1: for S be TopStruct holds ex T be strict TopSpace st the carrier of T = the carrier of S & the topology of S is prebasis of T

    proof

      let S be TopStruct;

      set T = TopStruct (# the carrier of S, ( UniCl ( FinMeetCl the topology of S)) #);

      

       A1: { {} , {} } = { {} } by ENUMSET1: 29;

      now

        assume

         A2: the carrier of S = {} ;

        then the topology of S = {} or the topology of S = { {} } by ZFMISC_1: 1, ZFMISC_1: 33;

        then ( FinMeetCl the topology of S) = { {} } by A1, A2, Th11, Th17;

        then ( UniCl ( FinMeetCl the topology of S)) = { {} } by A1, Th11;

        hence T is discrete TopStruct by A2, TDLAT_3:def 1, ZFMISC_1: 1;

      end;

      then

      reconsider T as strict TopSpace by CANTOR_1: 15;

      take T;

      

       A3: the topology of S c= ( FinMeetCl the topology of S) by CANTOR_1: 4;

      ( FinMeetCl the topology of S) c= the topology of T by CANTOR_1: 1;

      then

       A4: the topology of S c= the topology of T by A3;

      ( FinMeetCl the topology of S) is Basis of T by Th22;

      hence thesis by A4, CANTOR_1:def 4, TOPS_2: 64;

    end;

    begin

    definition

      let T be TopStruct;

      :: YELLOW_9:def5

      mode TopExtension of T -> TopSpace means

      : Def5: the carrier of T = the carrier of it & the topology of T c= the topology of it ;

      existence

      proof

        consider R be strict TopSpace such that

         A1: the carrier of R = the carrier of T and

         A2: the topology of T is prebasis of R by Lm1;

        take R;

        thus thesis by A1, A2, TOPS_2: 64;

      end;

    end

    theorem :: YELLOW_9:53

    

     Th53: for S be TopStruct holds ex T be TopExtension of S st T is strict & the topology of S is prebasis of T

    proof

      let S be TopStruct;

      consider T be strict TopSpace such that

       A1: the carrier of T = the carrier of S and

       A2: the topology of S is prebasis of T by Lm1;

      the topology of S c= the topology of T by A2, TOPS_2: 64;

      then

      reconsider T as TopExtension of S by A1, Def5;

      take T;

      thus thesis by A2;

    end;

    registration

      let T be TopStruct;

      cluster strict discrete for TopExtension of T;

      existence

      proof

        reconsider S = ( bool the carrier of T) as Subset-Family of T;

        reconsider S as Subset-Family of T;

        set R = TopStruct (# the carrier of T, S #);

        

         A1: R is discrete TopStruct by TDLAT_3:def 1;

        the topology of T c= S;

        then R is TopExtension of T by A1, Def5;

        hence thesis by A1;

      end;

    end

    definition

      let T1,T2 be TopStruct;

      :: YELLOW_9:def6

      mode Refinement of T1,T2 -> TopSpace means

      : Def6: the carrier of it = (the carrier of T1 \/ the carrier of T2) & (the topology of T1 \/ the topology of T2) is prebasis of it ;

      existence

      proof

        set c1 = the carrier of T1, c2 = the carrier of T2;

        set t1 = the topology of T1, t2 = the topology of T2;

        

         A1: ( bool c1) c= ( bool (c1 \/ c2)) by XBOOLE_1: 7, ZFMISC_1: 67;

        

         A2: ( bool c2) c= ( bool (c1 \/ c2)) by XBOOLE_1: 7, ZFMISC_1: 67;

        

         A3: t1 c= ( bool (c1 \/ c2)) by A1;

        t2 c= ( bool (c1 \/ c2)) by A2;

        then

        reconsider t = (t1 \/ t2) as Subset-Family of (c1 \/ c2) by A3, XBOOLE_1: 8;

        reconsider t as Subset-Family of (c1 \/ c2);

        set S = TopStruct (# (c1 \/ c2), t #);

        consider T be TopExtension of S such that

         A4: T is strict and

         A5: t is prebasis of T by Th53;

        reconsider T as strict TopExtension of S by A4;

        take T;

        thus thesis by A5, Def5;

      end;

    end

    registration

      let T1 be non empty TopStruct, T2 be TopStruct;

      cluster -> non empty for Refinement of T1, T2;

      coherence

      proof

        let T be Refinement of T1, T2;

        the carrier of T = (the carrier of T2 \/ the carrier of T1) by Def6;

        hence the carrier of T is non empty;

      end;

      cluster -> non empty for Refinement of T2, T1;

      coherence

      proof

        let T be Refinement of T2, T1;

        the carrier of T = (the carrier of T2 \/ the carrier of T1) by Def6;

        hence the carrier of T is non empty;

      end;

    end

    theorem :: YELLOW_9:54

    for T1,T2 be TopStruct, T,T9 be Refinement of T1, T2 holds the TopStruct of T = the TopStruct of T9

    proof

      let T1,T2 be TopStruct, T,T9 be Refinement of T1, T2;

      

       A1: the carrier of T = (the carrier of T1 \/ the carrier of T2) by Def6;

      

       A2: (the topology of T1 \/ the topology of T2) is prebasis of T by Def6;

      

       A3: the carrier of T9 = (the carrier of T1 \/ the carrier of T2) by Def6;

      (the topology of T1 \/ the topology of T2) is prebasis of T9 by Def6;

      hence thesis by A1, A2, A3, Th26;

    end;

    theorem :: YELLOW_9:55

    for T1,T2 be TopStruct, T be Refinement of T1, T2 holds T is Refinement of T2, T1

    proof

      let T1,T2 be TopStruct, T be Refinement of T1, T2;

      

       A1: the carrier of T = (the carrier of T1 \/ the carrier of T2) by Def6;

      (the topology of T1 \/ the topology of T2) is prebasis of T by Def6;

      hence thesis by A1, Def6;

    end;

    theorem :: YELLOW_9:56

    for T1,T2 be TopStruct, T be Refinement of T1, T2 holds for X be Subset-Family of T st X = (the topology of T1 \/ the topology of T2) holds the topology of T = ( UniCl ( FinMeetCl X))

    proof

      let T1,T2 be TopStruct, T be Refinement of T1, T2;

      let X be Subset-Family of T;

      assume X = (the topology of T1 \/ the topology of T2);

      then X is prebasis of T by Def6;

      then ( FinMeetCl X) is Basis of T by Th23;

      hence thesis by Th22;

    end;

    theorem :: YELLOW_9:57

    for T1,T2 be TopStruct st the carrier of T1 = the carrier of T2 holds for T be Refinement of T1, T2 holds T is TopExtension of T1 & T is TopExtension of T2

    proof

      let T1,T2 be TopStruct such that

       A1: the carrier of T1 = the carrier of T2;

      let T be Refinement of T1, T2;

      

       A2: the carrier of T = (the carrier of T1 \/ the carrier of T2) by Def6

      .= the carrier of T1 by A1;

      

       A3: (the topology of T1 \/ the topology of T2) is prebasis of T by Def6;

      

       A4: the topology of T1 c= (the topology of T1 \/ the topology of T2) by XBOOLE_1: 7;

      

       A5: the topology of T2 c= (the topology of T1 \/ the topology of T2) by XBOOLE_1: 7;

      

       A6: (the topology of T1 \/ the topology of T2) c= the topology of T by A3, TOPS_2: 64;

      then

       A7: the topology of T1 c= the topology of T by A4;

      the topology of T2 c= the topology of T by A5, A6;

      hence thesis by A1, A2, A7, Def5;

    end;

    theorem :: YELLOW_9:58

    for T1,T2 be non empty TopSpace, T be Refinement of T1, T2 holds for B1 be prebasis of T1, B2 be prebasis of T2 holds ((B1 \/ B2) \/ {the carrier of T1, the carrier of T2}) is prebasis of T

    proof

      let T1,T2 be non empty TopSpace, T be Refinement of T1, T2;

      let B1 be prebasis of T1, B2 be prebasis of T2;

      reconsider B = (the topology of T1 \/ the topology of T2) as prebasis of T by Def6;

      set cT1 = the carrier of T1, cT2 = the carrier of T2;

      reconsider C1 = (B1 \/ {cT1}) as prebasis of T1 by Th29;

      reconsider C2 = (B2 \/ {cT2}) as prebasis of T2 by Th29;

      

       A1: B1 c= the topology of T1 by TOPS_2: 64;

      

       A2: C1 c= the topology of T1 by TOPS_2: 64;

      

       A3: B2 c= the topology of T2 by TOPS_2: 64;

      

       A4: C2 c= the topology of T2 by TOPS_2: 64;

      

       A5: cT1 in the topology of T1 by PRE_TOPC:def 1;

      

       A6: cT2 in the topology of T2 by PRE_TOPC:def 1;

      

       A7: (B1 \/ B2) c= B by A1, A3, XBOOLE_1: 13;

      

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

      

       A9: cT1 in B by A5, XBOOLE_0:def 3;

      

       A10: cT2 in B by A6, XBOOLE_0:def 3;

      

       A11: (B1 \/ B2) c= the topology of T by A7, A8;

      

       A12: {cT1, cT2} c= the topology of T by A8, A9, A10, ZFMISC_1: 32;

      

       A13: {cT1, cT2} c= B by A9, A10, ZFMISC_1: 32;

      ((B1 \/ B2) \/ {cT1, cT2}) c= the topology of T by A11, A12, XBOOLE_1: 8;

      then

      reconsider BB = ((B1 \/ B2) \/ {cT1, cT2}) as Subset-Family of T by XBOOLE_1: 1;

      

       A14: the topology of T1 c= B by XBOOLE_1: 7;

      

       A15: the topology of T2 c= B by XBOOLE_1: 7;

      

       A16: C1 c= B by A2, A14;

      C2 c= B by A4, A15;

      then

      reconsider D1 = C1, D2 = C2 as Subset-Family of T by A16, XBOOLE_1: 1;

      reconsider D1, D2 as Subset-Family of T;

      reconsider D1, D2 as Subset-Family of T;

      

       A17: ( UniCl ( FinMeetCl BB)) = ( UniCl ( FinMeetCl ( FinMeetCl BB))) by CANTOR_1: 11

      .= ( UniCl ( FinMeetCl ( UniCl ( FinMeetCl BB)))) by Th21;

      

       A18: ( FinMeetCl B) is Basis of T by Th23;

      

       A19: ( FinMeetCl C1) is Basis of T1 by Th23;

      

       A20: ( FinMeetCl C2) is Basis of T2 by Th23;

      

       A21: ( UniCl ( FinMeetCl B)) = the topology of T by A18, Th22;

      

       A22: ( UniCl ( FinMeetCl C1)) = the topology of T1 by A19, Th22;

      

       A23: ( UniCl ( FinMeetCl C2)) = the topology of T2 by A20, Th22;

      

       A24: B1 c= (B1 \/ B2) by XBOOLE_1: 7;

      

       A25: B2 c= (B1 \/ B2) by XBOOLE_1: 7;

      

       A26: {cT1} c= {cT1, cT2} by ZFMISC_1: 7;

      

       A27: {cT2} c= {cT1, cT2} by ZFMISC_1: 7;

      

       A28: D1 c= BB by A24, A26, XBOOLE_1: 13;

      

       A29: D2 c= BB by A25, A27, XBOOLE_1: 13;

      BB c= B by A7, A13, XBOOLE_1: 8;

      then

       A30: ( FinMeetCl BB) c= ( FinMeetCl B) by CANTOR_1: 14;

      

       A31: ( FinMeetCl D1) c= ( FinMeetCl BB) by A28, CANTOR_1: 14;

      

       A32: ( FinMeetCl D2) c= ( FinMeetCl BB) by A29, CANTOR_1: 14;

      

       A33: ( UniCl ( FinMeetCl BB)) c= the topology of T by A21, A30, CANTOR_1: 9;

      

       A34: cT1 in {cT1} by TARSKI:def 1;

      

       A35: cT2 in {cT2} by TARSKI:def 1;

      

       A36: cT1 in C1 by A34, XBOOLE_0:def 3;

      

       A37: cT2 in C2 by A35, XBOOLE_0:def 3;

      

       A38: ( FinMeetCl D1) = ( {the carrier of T} \/ ( FinMeetCl C1)) by A36, Th20;

      

       A39: ( FinMeetCl D2) = ( {the carrier of T} \/ ( FinMeetCl C2)) by A37, Th20;

      

       A40: ( FinMeetCl C1) c= ( FinMeetCl D1) by A38, XBOOLE_1: 7;

      

       A41: ( FinMeetCl C2) c= ( FinMeetCl D2) by A39, XBOOLE_1: 7;

      

       A42: ( FinMeetCl C1) c= ( FinMeetCl BB) by A31, A40;

      

       A43: ( FinMeetCl C2) c= ( FinMeetCl BB) by A32, A41;

      

       A44: the topology of T1 c= ( UniCl ( FinMeetCl BB)) by A22, A42, Th19;

      the topology of T2 c= ( UniCl ( FinMeetCl BB)) by A23, A43, Th19;

      then B c= ( UniCl ( FinMeetCl BB)) by A44, XBOOLE_1: 8;

      then ( FinMeetCl B) c= ( FinMeetCl ( UniCl ( FinMeetCl BB))) by CANTOR_1: 14;

      then the topology of T c= ( UniCl ( FinMeetCl BB)) by A17, A21, CANTOR_1: 9;

      then the topology of T = ( UniCl ( FinMeetCl BB)) by A33;

      then ( FinMeetCl BB) is Basis of T by Th22;

      hence thesis by Th23;

    end;

    theorem :: YELLOW_9:59

    

     Th59: for T1,T2 be non empty TopSpace holds for B1 be Basis of T1, B2 be Basis of T2 holds for T be Refinement of T1, T2 holds ((B1 \/ B2) \/ ( INTERSECTION (B1,B2))) is Basis of T

    proof

      let T1,T2 be non empty TopSpace;

      let B1 be Basis of T1, B2 be Basis of T2;

      let T be Refinement of T1, T2;

      set BB = ((B1 \/ B2) \/ ( INTERSECTION (B1,B2)));

      reconsider B = (the topology of T1 \/ the topology of T2) as prebasis of T by Def6;

      

       A1: ( FinMeetCl B) is Basis of T by Th23;

      

       A2: (the carrier of T1 \/ the carrier of T2) = the carrier of T by Def6;

      

       A3: B1 c= the topology of T1 by TOPS_2: 64;

      

       A4: B2 c= the topology of T2 by TOPS_2: 64;

      

       A5: the topology of T1 c= B by XBOOLE_1: 7;

      

       A6: the topology of T2 c= B by XBOOLE_1: 7;

      

       A7: B1 c= B by A3, A5;

      

       A8: B2 c= B by A4, A6;

      

       A9: B c= ( FinMeetCl B) by CANTOR_1: 4;

      then

       A10: B1 c= ( FinMeetCl B) by A7;

      

       A11: B2 c= ( FinMeetCl B) by A8, A9;

      

       A12: (B1 \/ B2) c= B by A3, A4, XBOOLE_1: 13;

      

       A13: ( INTERSECTION (B1,B2)) c= ( FinMeetCl B) by A10, A11, CANTOR_1: 13;

      (B1 \/ B2) c= ( FinMeetCl B) by A9, A12;

      then

       A14: BB c= ( FinMeetCl B) by A13, XBOOLE_1: 8;

      

       A15: ( FinMeetCl B) c= the topology of T by A1, TOPS_2: 64;

      reconsider BB as Subset-Family of T by A14, XBOOLE_1: 1;

      now

        let A be Subset of T such that

         A16: A is open;

        let p be Point of T;

        assume p in A;

        then

        consider a be Subset of T such that

         A17: a in ( FinMeetCl B) and

         A18: p in a and

         A19: a c= A by A1, A16, Th31;

        consider Y be Subset-Family of T such that

         A20: Y c= B and

         A21: Y is finite and

         A22: a = ( Intersect Y) by A17, CANTOR_1:def 3;

        reconsider Y1 = (Y /\ the topology of T1) as Subset-Family of T1;

        reconsider Y2 = (Y /\ the topology of T2) as Subset-Family of T2;

        

         A23: Y = (B /\ Y) by A20, XBOOLE_1: 28

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

        the carrier of T1 c= the carrier of T1;

        then

        reconsider cT1 = the carrier of T1 as Subset of T1;

        the carrier of T2 c= the carrier of T2;

        then

        reconsider cT2 = the carrier of T2 as Subset of T2;

        

         A24: cT1 in the topology of T1 by PRE_TOPC:def 1;

        

         A25: cT2 in the topology of T2 by PRE_TOPC:def 1;

        

         A26: cT1 is open by A24;

        

         A27: cT2 is open by A25;

        thus ex a be Subset of T st a in BB & p in a & a c= A

        proof

          per cases by A2, XBOOLE_0:def 3;

            suppose

             A28: (Y1 \/ Y2) = {} & p in cT1;

            then

            consider b1 be Subset of T1 such that

             A29: b1 in B1 and

             A30: p in b1 and b1 c= cT1 by A26, Th31;

            

             A31: b1 in (B1 \/ B2) by A29, XBOOLE_0:def 3;

            

             A32: a = the carrier of T by A22, A23, A28, SETFAM_1:def 9;

            b1 in BB by A31, XBOOLE_0:def 3;

            hence thesis by A19, A30, A32, XBOOLE_1: 1;

          end;

            suppose

             A33: (Y1 \/ Y2) = {} & p in cT2;

            then

            consider b2 be Subset of T2 such that

             A34: b2 in B2 and

             A35: p in b2 and b2 c= cT2 by A27, Th31;

            

             A36: b2 in (B1 \/ B2) by A34, XBOOLE_0:def 3;

            

             A37: a = the carrier of T by A22, A23, A33, SETFAM_1:def 9;

            b2 in BB by A36, XBOOLE_0:def 3;

            hence thesis by A19, A35, A37, XBOOLE_1: 1;

          end;

            suppose

             A38: Y1 = {} & Y2 <> {} & Y <> {} ;

            

            then

             A39: a = ( meet Y2) by A22, A23, SETFAM_1:def 9

            .= ( Intersect Y2) by A38, SETFAM_1:def 9;

            Y2 c= the topology of T2 by XBOOLE_1: 17;

            then a in ( FinMeetCl the topology of T2) by A21, A39, CANTOR_1:def 3;

            then

             A40: a in the topology of T2 by CANTOR_1: 5;

            the topology of T2 = ( UniCl B2) by Th22;

            then

            consider Z be Subset-Family of T2 such that

             A41: Z c= B2 and

             A42: a = ( union Z) by A40, CANTOR_1:def 1;

            consider z be set such that

             A43: p in z and

             A44: z in Z by A18, A42, TARSKI:def 4;

            z in (B1 \/ B2) by A41, A44, XBOOLE_0:def 3;

            then

             A45: z in BB by XBOOLE_0:def 3;

            z c= a by A42, A44, ZFMISC_1: 74;

            hence thesis by A19, A43, A45, XBOOLE_1: 1;

          end;

            suppose

             A46: Y1 <> {} & Y2 = {} & Y <> {} ;

            

            then

             A47: a = ( meet Y1) by A22, A23, SETFAM_1:def 9

            .= ( Intersect Y1) by A46, SETFAM_1:def 9;

            Y1 c= the topology of T1 by XBOOLE_1: 17;

            then a in ( FinMeetCl the topology of T1) by A21, A47, CANTOR_1:def 3;

            then

             A48: a in the topology of T1 by CANTOR_1: 5;

            the topology of T1 = ( UniCl B1) by Th22;

            then

            consider Z be Subset-Family of T1 such that

             A49: Z c= B1 and

             A50: a = ( union Z) by A48, CANTOR_1:def 1;

            consider z be set such that

             A51: p in z and

             A52: z in Z by A18, A50, TARSKI:def 4;

            z in (B1 \/ B2) by A49, A52, XBOOLE_0:def 3;

            then

             A53: z in BB by XBOOLE_0:def 3;

            z c= a by A50, A52, ZFMISC_1: 74;

            hence thesis by A19, A51, A53, XBOOLE_1: 1;

          end;

            suppose

             A54: Y1 <> {} & Y2 <> {} & Y <> {} ;

            

            then

             A55: a = ( meet Y) by A22, SETFAM_1:def 9

            .= (( meet Y1) /\ ( meet Y2)) by A23, A54, SETFAM_1: 9

            .= (( meet Y1) /\ ( Intersect Y2)) by A54, SETFAM_1:def 9

            .= (( Intersect Y1) /\ ( Intersect Y2)) by A54, SETFAM_1:def 9;

            

             A56: Y1 c= the topology of T1 by XBOOLE_1: 17;

            

             A57: Y2 c= the topology of T2 by XBOOLE_1: 17;

            

             A58: ( Intersect Y1) in ( FinMeetCl the topology of T1) by A21, A56, CANTOR_1:def 3;

            

             A59: ( Intersect Y2) in ( FinMeetCl the topology of T2) by A21, A57, CANTOR_1:def 3;

            

             A60: ( Intersect Y1) in the topology of T1 by A58, CANTOR_1: 5;

            

             A61: the topology of T1 = ( UniCl B1) by Th22;

            

             A62: ( Intersect Y2) in the topology of T2 by A59, CANTOR_1: 5;

            

             A63: the topology of T2 = ( UniCl B2) by Th22;

            consider Z1 be Subset-Family of T1 such that

             A64: Z1 c= B1 and

             A65: ( Intersect Y1) = ( union Z1) by A60, A61, CANTOR_1:def 1;

            p in ( Intersect Y1) by A18, A55, XBOOLE_0:def 4;

            then

            consider z1 be set such that

             A66: p in z1 and

             A67: z1 in Z1 by A65, TARSKI:def 4;

            consider Z2 be Subset-Family of T2 such that

             A68: Z2 c= B2 and

             A69: ( Intersect Y2) = ( union Z2) by A62, A63, CANTOR_1:def 1;

            p in ( Intersect Y2) by A18, A55, XBOOLE_0:def 4;

            then

            consider z2 be set such that

             A70: p in z2 and

             A71: z2 in Z2 by A69, TARSKI:def 4;

            

             A72: (z1 /\ z2) in ( INTERSECTION (B1,B2)) by A64, A67, A68, A71, SETFAM_1:def 5;

            

             A73: z1 c= ( union Z1) by A67, ZFMISC_1: 74;

            

             A74: z2 c= ( union Z2) by A71, ZFMISC_1: 74;

            

             A75: (z1 /\ z2) in BB by A72, XBOOLE_0:def 3;

            

             A76: (z1 /\ z2) c= a by A55, A65, A69, A73, A74, XBOOLE_1: 27;

            p in (z1 /\ z2) by A66, A70, XBOOLE_0:def 4;

            hence thesis by A19, A75, A76, XBOOLE_1: 1;

          end;

        end;

      end;

      hence thesis by A14, A15, Th32, XBOOLE_1: 1;

    end;

    theorem :: YELLOW_9:60

    

     Th60: for T1,T2 be non empty TopSpace st the carrier of T1 = the carrier of T2 holds for T be Refinement of T1, T2 holds ( INTERSECTION (the topology of T1,the topology of T2)) is Basis of T

    proof

      let T1,T2 be non empty TopSpace such that

       A1: the carrier of T1 = the carrier of T2;

      let T be Refinement of T1, T2;

      set B1 = the topology of T1, B2 = the topology of T2;

      ( UniCl B1) = B1 by CANTOR_1: 6;

      then

      reconsider B1 as Basis of T1 by Th22;

      ( UniCl B2) = B2 by CANTOR_1: 6;

      then

      reconsider B2 as Basis of T2 by Th22;

      

       A2: ((B1 \/ B2) \/ ( INTERSECTION (B1,B2))) is Basis of T by Th59;

      

       A3: the carrier of T1 in B1 by PRE_TOPC:def 1;

      

       A4: the carrier of T2 in B2 by PRE_TOPC:def 1;

      

       A5: B1 c= ( INTERSECTION (B1,B2))

      proof

        let a be object;

        reconsider aa = a as set by TARSKI: 1;

        assume

         A6: a in B1;

        then (aa /\ the carrier of T1) in ( INTERSECTION (B1,B2)) by A1, A4, SETFAM_1:def 5;

        hence thesis by A6, XBOOLE_1: 28;

      end;

      B2 c= ( INTERSECTION (B1,B2))

      proof

        let a be object;

        reconsider aa = a as set by TARSKI: 1;

        assume

         A7: a in B2;

        then (aa /\ the carrier of T2) in ( INTERSECTION (B1,B2)) by A1, A3, SETFAM_1:def 5;

        hence thesis by A7, XBOOLE_1: 28;

      end;

      hence thesis by A2, A5, XBOOLE_1: 8, XBOOLE_1: 12;

    end;

    theorem :: YELLOW_9:61

    for L be non empty RelStr holds for T1,T2 be correct TopAugmentation of L holds for T be Refinement of T1, T2 holds ( INTERSECTION (the topology of T1,the topology of T2)) is Basis of T

    proof

      let L be non empty RelStr;

      let T1,T2 be correct TopAugmentation of L;

      

       A1: the RelStr of T1 = the RelStr of L by Def4;

       the RelStr of T2 = the RelStr of L by Def4;

      hence thesis by A1, Th60;

    end;