let T be non empty TopSpace; :: thesis: for L1 being lower-bounded continuous LATTICE st InclPoset the topology of T = L1 holds
for B1 being Basis of T
for B2 being Subset of L1 st B1 = B2 holds
finsups B2 is with_bottom CLbasis of L1
let L1 be lower-bounded continuous LATTICE; :: thesis: ( InclPoset the topology of T = L1 implies for B1 being Basis of T
for B2 being Subset of L1 st B1 = B2 holds
finsups B2 is with_bottom CLbasis of L1 )
assume A1: InclPoset the topology of T = L1 ; :: thesis: for B1 being Basis of T
for B2 being Subset of L1 st B1 = B2 holds
finsups B2 is with_bottom CLbasis of L1
let B1 be Basis of T; :: thesis: for B2 being Subset of L1 st B1 = B2 holds
finsups B2 is with_bottom CLbasis of L1
let B2 be Subset of L1; :: thesis: ( B1 = B2 implies finsups B2 is with_bottom CLbasis of L1 )
assume A2: B1 = B2 ; :: thesis: finsups B2 is with_bottom CLbasis of L1
A3: for x, y being Element of L1 st not y <= x holds
ex b being Element of L1 st
( b in finsups B2 & not b <= x & b <= y )

proof

let x, y be Element of L1; :: thesis: ( not y <= x implies ex b being Element of L1 st
( b in finsups B2 & not b <= x & b <= y ) )
y in the carrier of L1 ;
then A4: y in the topology of T by A1, YELLOW_1:1;
then reconsider y1 = y as Subset of T ;
assume not y <= x ; :: thesis: ex b being Element of L1 st
( b in finsups B2 & not b <= x & b <= y )
then not y c= x by A1, YELLOW_1:3;
then consider v being object such that
A5: v in y and
A6: not v in x ;
v in y1 by A5;
then reconsider v = v as Point of T ;
y1 is open by A4, PRE_TOPC:def 2;
then consider b being Subset of T such that
A7: b in B1 and
A8: v in b and
A9: b c= y1 by A5, YELLOW_9:31;
reconsider b = b as Element of L1 by A2, A7;
for z being object st z in {b} holds
z in B2 by A2, A7, TARSKI:def 1;
then A10: {b} is finite Subset of B2 by TARSKI:def 3;
take b ; :: thesis: ( b in finsups B2 & not b <= x & b <= y )
( ex_sup_of {b},L1 & b = "\/" ({b},L1) ) by YELLOW_0:38, YELLOW_0:39;
then b in { ("\/" (Y,L1)) where Y is finite Subset of B2 : ex_sup_of Y,L1 } by A10;
hence b in finsups B2 by WAYBEL_0:def 27; :: thesis: ( not b <= x & b <= y )
not b c= x by A6, A8;
hence not b <= x by A1, YELLOW_1:3; :: thesis: b <= y
thus b <= y by A1, A9, YELLOW_1:3; :: thesis: verum

end;

now :: thesis: for x, y being Element of L1 st x in finsups B2 & y in finsups B2 holds
sup {x,y} in finsups B2

let x, y be Element of L1; :: thesis: ( x in finsups B2 & y in finsups B2 implies sup {x,y} in finsups B2 )
assume that
A11: x in finsups B2 and
A12: y in finsups B2 ; :: thesis: sup {x,y} in finsups B2
y in { ("\/" (Y,L1)) where Y is finite Subset of B2 : ex_sup_of Y,L1 } by A12, WAYBEL_0:def 27;
then consider Y2 being finite Subset of B2 such that
A13: y = "\/" (Y2,L1) and
A14: ex_sup_of Y2,L1 ;
x in { ("\/" (Y,L1)) where Y is finite Subset of B2 : ex_sup_of Y,L1 } by A11, WAYBEL_0:def 27;
then consider Y1 being finite Subset of B2 such that
A15: x = "\/" (Y1,L1) and
A16: ex_sup_of Y1,L1 ;
( ex_sup_of Y1 \/ Y2,L1 & "\/" ((Y1 \/ Y2),L1) = ("\/" (Y1,L1)) "\/" ("\/" (Y2,L1)) ) by A16, A14, YELLOW_2:3;
then x "\/" y in { ("\/" (Y,L1)) where Y is finite Subset of B2 : ex_sup_of Y,L1 } by A15, A13;
then x "\/" y in finsups B2 by WAYBEL_0:def 27;
hence sup {x,y} in finsups B2 by YELLOW_0:41; :: thesis: verum

end;

then A17: finsups B2 is join-closed by WAYBEL23:18;
( {} c= B2 & ex_sup_of {} ,L1 ) by YELLOW_0:42;
then "\/" ({},L1) in { ("\/" (Y,L1)) where Y is finite Subset of B2 : ex_sup_of Y,L1 } ;
then Bottom L1 in finsups B2 by WAYBEL_0:def 27;
hence finsups B2 is with_bottom CLbasis of L1 by A17, A3, WAYBEL23:49, WAYBEL23:def 8; :: thesis: verum