let T be non empty TopSpace-like TopRelStr ; :: thesis: ( T is lower iff { ((uparrow F) ` ) where F is Subset of T : F is finite } is Basis of T )
reconsider T' = T as non empty RelStr ;
set BB = { ((uparrow x) ` ) where x is Element of T : verum } ;
set A = { ((uparrow F) ` ) where F is Subset of T : F is finite } ;
{ ((uparrow x) ` ) where x is Element of T : verum } c= bool the carrier of T
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { ((uparrow x) ` ) where x is Element of T : verum } or x in bool the carrier of T )
assume x in { ((uparrow x) ` ) where x is Element of T : verum } ; :: thesis: x in bool the carrier of T
then ex y being Element of T st x = (uparrow y) ` ;
hence x in bool the carrier of T ; :: thesis: verum
end;
then reconsider BB = { ((uparrow x) ` ) where x is Element of T : verum } as Subset-Family of T ;
reconsider BB = BB as Subset-Family of T ;
A1: { ((uparrow F) ` ) where F is Subset of T : F is finite } = FinMeetCl BB
proof
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: FinMeetCl BB c= { ((uparrow F) ` ) where F is Subset of T : F is finite }
let a be set ; :: thesis: ( a in { ((uparrow F) ` ) where F is Subset of T : F is finite } implies a in FinMeetCl BB )
assume a in { ((uparrow F) ` ) where F is Subset of T : F is finite } ; :: thesis: a in FinMeetCl BB
then consider F being Subset of T such that
A2: a = (uparrow F) ` and
A3: F is finite ;
set Y = { (uparrow x) where x is Element of T : x in F } ;
{ (uparrow x) where x is Element of T : x in F } c= bool the carrier of T
proof
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { (uparrow x) where x is Element of T : x in F } or a in bool the carrier of T )
assume a in { (uparrow x) where x is Element of T : x in F } ; :: thesis: a in bool the carrier of T
then ex x being Element of T st
( a = uparrow x & x in F ) ;
hence a in bool the carrier of T ; :: thesis: verum
end;
then reconsider Y = { (uparrow x) where x is Element of T : x in F } as Subset-Family of T ;
reconsider Y = Y as Subset-Family of T ;
reconsider Y' = Y as Subset-Family of T' ;
deffunc H1( Element of T') -> Element of bool the carrier of T' = uparrow $1;
A4: Y' = { H1(x) where x is Element of T' : x in F } ;
A5: COMPLEMENT Y' = { (H1(x) ` ) where x is Element of T' : x in F } from YELLOW_9:sch 2(A4);
 uparrow F = union Y by YELLOW_9:4;
then A6: a = Intersect (COMPLEMENT Y) by A2, YELLOW_8:15;
deffunc H2( Element of T) -> Element of bool the carrier of T = (uparrow $1) ` ;
A7: { H2(x) where x is Element of T : x in F } is finite from FRAENKEL:sch 21(A3);
 COMPLEMENT Y c= BB
proof
let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in COMPLEMENT Y or b in BB )
assume b in COMPLEMENT Y ; :: thesis: b in BB
then ex x being Element of T st
( b = (uparrow x) ` & x in F ) by A5;
hence b in BB ; :: thesis: verum
end;
hence a in FinMeetCl BB by A5, A6, A7, CANTOR_1:def 4; :: thesis: verum
end;
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in FinMeetCl BB or a in { ((uparrow F) ` ) where F is Subset of T : F is finite } )
assume a in FinMeetCl BB ; :: thesis: a in { ((uparrow F) ` ) where F is Subset of T : F is finite }
then consider Y being Subset-Family of T such that
A8: ( Y c= BB & Y is finite & a = Intersect Y ) by CANTOR_1:def 4;
defpred S1[ set , set ] means ex x being Element of T st
( x = $2 & $1 = (uparrow x) ` );
A9: now
let y be set ; :: thesis: ( y in Y implies ex b being set st
( b in the carrier of T & S1[y,b] ) )
assume y in Y ; :: thesis: ex b being set st
( b in the carrier of T & S1[y,b] )
then y in BB by A8;
then ex x being Element of T st y = (uparrow x) ` ;
hence ex b being set st
( b in the carrier of T & S1[y,b] ) ; :: thesis: verum
end;
consider f being Function such that
A10: ( dom f = Y & rng f c= the carrier of T ) and
A11: for y being set st y in Y holds
S1[y,f . y] from WELLORD2:sch 1(A9);
 reconsider F = rng f as Subset of T by A10;
set X = { (uparrow x) where x is Element of T : x in F } ;
{ (uparrow x) where x is Element of T : x in F } c= bool the carrier of T
proof
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { (uparrow x) where x is Element of T : x in F } or a in bool the carrier of T )
assume a in { (uparrow x) where x is Element of T : x in F } ; :: thesis: a in bool the carrier of T
then ex x being Element of T st
( a = uparrow x & x in F ) ;
hence a in bool the carrier of T ; :: thesis: verum
end;
then reconsider X = { (uparrow x) where x is Element of T : x in F } as Subset-Family of T ;
reconsider X = X as Subset-Family of T ;
reconsider X' = X as Subset-Family of T' ;
deffunc H1( Element of T') -> Element of bool the carrier of T' = uparrow $1;
A12: X' = { H1(x) where x is Element of T' : x in F } ;
A13: COMPLEMENT X' = { (H1(x) ` ) where x is Element of T' : x in F } from YELLOW_9:sch 2(A12);
 A14: COMPLEMENT X = Y
proof
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: Y c= COMPLEMENT X
let a be set ; :: thesis: ( a in COMPLEMENT X implies a in Y )
assume a in COMPLEMENT X ; :: thesis: a in Y
then consider x being Element of T' such that
A15: ( a = (uparrow x) ` & x in F ) by A13;
consider y being set such that
A16: ( y in Y & x = f . y ) by A10, A15, FUNCT_1:def 5;
consider z being Element of T such that
A17: ( z = f . y & y = (uparrow z) ` ) by A11, A16;
thus a in Y by A15, A16, A17; :: thesis: verum
end;
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in Y or a in COMPLEMENT X )
assume A18: a in Y ; :: thesis: a in COMPLEMENT X
then consider z being Element of T such that
A19: ( z = f . a & a = (uparrow z) ` ) by A11;
z in F by A10, A18, A19, FUNCT_1:def 5;
hence a in COMPLEMENT X by A13, A19; :: thesis: verum
end;
A20: F is finite by A8, A10, FINSET_1:26;
uparrow F = union X by YELLOW_9:4;
then a = (uparrow F) ` by A8, A14, YELLOW_8:15;
hence a in { ((uparrow F) ` ) where F is Subset of T : F is finite } by A20; :: thesis: verum
end;
( T is lower iff BB is prebasis of T ) by Def1;
hence ( T is lower iff { ((uparrow F) ` ) where F is Subset of T : F is finite } is Basis of T ) by A1, YELLOW_9:23; :: thesis: verum