let L1 be lower-bounded continuous sup-Semilattice; :: thesis: for T being Scott TopAugmentation of L1 holds CLweight L1 c= weight T
let T be Scott TopAugmentation of L1; :: thesis: CLweight L1 c= weight T
consider B1 being Basis of T such that
A1: card B1 = weight T by WAYBEL23:74;
{ (inf u) where u is Subset of T : u in B1 } c= the carrier of T

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { (inf u) where u is Subset of T : u in B1 } or z in the carrier of T )
assume z in { (inf u) where u is Subset of T : u in B1 } ; :: thesis: z in the carrier of T
then ex u being Subset of T st
( z = inf u & u in B1 ) ;
hence z in the carrier of T ; :: thesis: verum

end;

then reconsider B0 = { (inf u) where u is Subset of T : u in B1 } as Subset of T ;
set B2 = finsups B0;
defpred S₁[ object , object ] means ex y being Subset of T st
( $1 = y & $2 = inf y );
A2: for x being object st x in B1 holds
ex y being object st
( y in B0 & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in B1 implies ex y being object st
( y in B0 & S₁[x,y] ) )
assume A3: x in B1 ; :: thesis: ex y being object st
( y in B0 & S₁[x,y] )
then reconsider z = x as Subset of T ;
take y = inf z; :: thesis: ( y in B0 & S₁[x,y] )
thus y in B0 by A3; :: thesis: S₁[x,y]
take z ; :: thesis: ( x = z & y = inf z )
thus ( x = z & y = inf z ) ; :: thesis: verum

end;

consider f being Function such that
A4: dom f = B1 and
rng f c= B0 and
A5: for x being object st x in B1 holds
S₁[x,f . x] from FUNCT_1:sch 6(A2);
B0 c= rng f

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in B0 or z in rng f )
assume z in B0 ; :: thesis: z in rng f
then consider u being Subset of T such that
A6: z = inf u and
A7: u in B1 ;
ex y being Subset of T st
( u = y & f . u = inf y ) by A5, A7;
hence z in rng f by A4, A6, A7, FUNCT_1:def 3; :: thesis: verum

end;

then A8: card B0 c= card B1 by A4, CARD_1:12;
A9: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def 4;

A10: now :: thesis: card (finsups B0) = card B0

per cases ( L1 is finite or L1 is infinite ) ;

suppose A11: L1 is finite ; :: thesis: card (finsups B0) = card B0

the carrier of L1 c= B0

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in the carrier of L1 or z in B0 )
assume z in the carrier of L1 ; :: thesis: z in B0
then reconsider z1 = z as Element of T by A9;
z1 <= z1 ;
then A12: z1 in uparrow z1 by WAYBEL_0:18;
T is finite by A9, A11;
then uparrow z1 is open by WAYBEL11:def 5;
then consider A being Subset of T such that
A13: A in B1 and
A14: z1 in A and
A15: A c= uparrow z1 by A12, YELLOW_9:31;
( ex_inf_of uparrow z1,T & ex_inf_of A,T ) by YELLOW_0:17;
then inf (uparrow z1) <= inf A by A15, YELLOW_0:35;
then A16: z1 <= inf A by WAYBEL_0:39;
inf A <= z1 by A14, YELLOW_2:22;
then z = inf A by A16, YELLOW_0:def 3;
hence z in B0 by A13; :: thesis: verum

end;

then ( B0 c= finsups B0 & finsups B0 c= B0 ) by A9, WAYBEL_0:50;
hence card (finsups B0) = card B0 by XBOOLE_0:def 10; :: thesis: verum

end;

suppose L1 is infinite ; :: thesis: card (finsups B0) = card B0

then T is infinite by A9;
then B0 is infinite by Th23, YELLOW15:30;
hence card (finsups B0) = card B0 by YELLOW15:27; :: thesis: verum

end;

end;

end;

( ex_sup_of {} ,T & {} is finite Subset of B0 ) by XBOOLE_1:2, YELLOW_0:42;
then "\/" ({},T) in { ("\/" (Y,T)) where Y is finite Subset of B0 : ex_sup_of Y,T } ;
then "\/" ({},T) in finsups B0 by WAYBEL_0:def 27;
then A17: Bottom L1 in finsups B0 by A9, YELLOW_0:26, YELLOW_0:42;
reconsider B2 = finsups B0 as Subset of L1 by A9;

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

let x, y be Element of L1; :: thesis: ( x in B2 & y in B2 implies sup {x,y} in B2 )
assume that
A18: x in B2 and
A19: y in B2 ; :: thesis: sup {x,y} in B2
y in { ("\/" (Y,T)) where Y is finite Subset of B0 : ex_sup_of Y,T } by A19, WAYBEL_0:def 27;
then consider Y2 being finite Subset of B0 such that
A20: y = "\/" (Y2,T) and
A21: ex_sup_of Y2,T ;
x in { ("\/" (Y,T)) where Y is finite Subset of B0 : ex_sup_of Y,T } by A18, WAYBEL_0:def 27;
then consider Y1 being finite Subset of B0 such that
A22: x = "\/" (Y1,T) and
A23: ex_sup_of Y1,T ;
A24: ex_sup_of Y1 \/ Y2,T by YELLOW_0:17;
sup {x,y} = x "\/" y by YELLOW_0:41
.= ("\/" (Y1,T)) "\/" ("\/" (Y2,T)) by A9, A22, A20, YELLOW12:10
.= "\/" ((Y1 \/ Y2),T) by A23, A21, YELLOW_2:3 ;
then sup {x,y} in { ("\/" (Y,T)) where Y is finite Subset of B0 : ex_sup_of Y,T } by A24;
hence sup {x,y} in B2 by WAYBEL_0:def 27; :: thesis: verum

end;

then reconsider B2 = B2 as join-closed Subset of L1 by WAYBEL23:18;
for x, y being Element of L1 st x << y holds
ex b being Element of L1 st
( b in B2 & x <= b & b << y )

proof

let x, y be Element of L1; :: thesis: ( x << y implies ex b being Element of L1 st
( b in B2 & x <= b & b << y ) )
reconsider x1 = x, y1 = y as Element of T by A9;
A25: B0 c= B2 by WAYBEL_0:50;
assume x << y ; :: thesis: ex b being Element of L1 st
( b in B2 & x <= b & b << y )
then y in wayabove x by WAYBEL_3:8;
then A26: y1 in wayabove x1 by A9, YELLOW12:13;
wayabove x1 is open by WAYBEL11:36;
then consider u being Subset of T such that
A27: u in B1 and
A28: y1 in u and
A29: u c= wayabove x1 by A26, YELLOW_9:31;
reconsider b = inf u as Element of L1 by A9;
take b ; :: thesis: ( b in B2 & x <= b & b << y )
b in B0 by A27;
hence b in B2 by A25; :: thesis: ( x <= b & b << y )
A30: wayabove x1 c= uparrow x1 by WAYBEL_3:11;
( ex_inf_of uparrow x1,T & ex_inf_of u,T ) by YELLOW_0:17;
then inf (uparrow x1) <= inf u by A29, A30, XBOOLE_1:1, YELLOW_0:35;
then x1 <= inf u by WAYBEL_0:39;
hence x <= b by A9, YELLOW_0:1; :: thesis: b << y
u is open by A27, YELLOW_8:10;
hence b << y by A9, A28, WAYBEL14:26, WAYBEL_8:8; :: thesis: verum

end;

then A31: B2 is CLbasis of L1 by A17, WAYBEL23:47;
B2 is with_bottom by A17, WAYBEL23:def 8;
then CLweight L1 c= card B0 by A10, A31, Th1;
hence CLweight L1 c= weight T by A1, A8; :: thesis: verum