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 )
set BB = { ((uparrow x) `) where x is Element of T : verum } ;
{ ((uparrow x) `) where x is Element of T : verum } c= bool the carrier of T

proof

let x be object ; :: 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 T9 = T as non empty RelStr ;
set A = { ((uparrow F) `) where F is Subset of T : F is finite } ;
reconsider BB = BB as Subset-Family of T ;
A1: { ((uparrow F) `) where F is Subset of T : F is finite } = FinMeetCl BB

proof

deffunc H₁( Element of T9) -> Element of bool the carrier of T9 = uparrow $1;
defpred S₁[ object , object ] means ex x being Element of T st
( x = $2 & $1 = (uparrow x) ` );

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 }

deffunc H₂( Element of T9) -> Element of bool the carrier of T9 = uparrow $1;
let a be object ; :: 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 object ; :: 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 ;
uparrow F = union Y by YELLOW_9:4;
then A4: a = Intersect (COMPLEMENT Y) by A2, YELLOW_8:6;
reconsider Y9 = Y as Subset-Family of T9 ;
A5: Y9 = { H₂(x) where x is Element of T9 : x in F } ;
A6: COMPLEMENT Y9 = { (H₂(x) `) where x is Element of T9 : x in F } from YELLOW_9:sch 2(A5);
A7: COMPLEMENT Y c= BB

proof

let b be object ; :: 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 A6;
hence b in BB ; :: thesis: verum

end;

deffunc H₃( Element of T) -> Element of bool the carrier of T = (uparrow $1) ` ;
{ H₃(x) where x is Element of T : x in F } is finite from FRAENKEL:sch 21(A3);
hence a in FinMeetCl BB by A7, A6, A4, CANTOR_1:def 3; :: thesis: verum

end;

let a be object ; :: 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 and
A9: Y is finite and
A10: a = Intersect Y by CANTOR_1:def 3;

A11: now :: thesis: for y being object st y in Y holds
ex b being object st
( b in the carrier of T & S₁[y,b] )

let y be object ; :: thesis: ( y in Y implies ex b being object st
( b in the carrier of T & S₁[y,b] ) )
assume y in Y ; :: thesis: ex b being object st
( b in the carrier of T & S₁[y,b] )
then y in BB by A8;
then ex x being Element of T st y = (uparrow x) ` ;
hence ex b being object st
( b in the carrier of T & S₁[y,b] ) ; :: thesis: verum

end;

consider f being Function such that
A12: ( dom f = Y & rng f c= the carrier of T ) and
A13: for y being object st y in Y holds
S₁[y,f . y] from FUNCT_1:sch 6(A11);
reconsider F = rng f as Subset of T by A12;
A14: F is finite by A9, A12, FINSET_1:8;
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 object ; :: 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 X9 = X as Subset-Family of T9 ;
A15: X9 = { H₁(x) where x is Element of T9 : x in F } ;
A16: COMPLEMENT X9 = { (H₁(x) `) where x is Element of T9 : x in F } from YELLOW_9:sch 2(A15);
A17: COMPLEMENT X = Y

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: Y c= COMPLEMENT X

let a be object ; :: thesis: ( a in COMPLEMENT X implies a in Y )
assume a in COMPLEMENT X ; :: thesis: a in Y
then consider x being Element of T9 such that
A18: a = (uparrow x) ` and
A19: x in F by A16;
consider y being object such that
A20: y in Y and
A21: x = f . y by A12, A19, FUNCT_1:def 3;
ex z being Element of T st
( z = f . y & y = (uparrow z) ` ) by A13, A20;
hence a in Y by A18, A20, A21; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Y or a in COMPLEMENT X )
assume A22: a in Y ; :: thesis: a in COMPLEMENT X
then consider z being Element of T such that
A23: z = f . a and
A24: a = (uparrow z) ` by A13;
z in F by A12, A22, A23, FUNCT_1:def 3;
hence a in COMPLEMENT X by A16, A24; :: thesis: verum

end;

uparrow F = union X by YELLOW_9:4;
then a = (uparrow F) ` by A10, A17, YELLOW_8:6;
hence a in { ((uparrow F) `) where F is Subset of T : F is finite } by A14; :: thesis: verum

end;

thus ( 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