let L1 be lower-bounded continuous sup-Semilattice; for T being Scott TopAugmentation of L1 holds CLweight L1 c= weight T
let T be Scott TopAugmentation of L1; 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
then reconsider B0 = { (inf u) where u is Subset of T : u in B1 } as Subset of T ;
set B2 = finsups B0;
defpred S1[ 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 & S1[x,y] )
proof
let x be
object ;
( x in B1 implies ex y being object st
( y in B0 & S1[x,y] ) )
assume A3:
x in B1
;
ex y being object st
( y in B0 & S1[x,y] )
then reconsider z =
x as
Subset of
T ;
take y =
inf z;
( y in B0 & S1[x,y] )
thus
y in B0
by A3;
S1[x,y]
take
z
;
( x = z & y = inf z )
thus
(
x = z &
y = inf z )
;
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
S1[x,f . x]
from FUNCT_1:sch 6(A2);
B0 c= rng f
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;
( 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 for x, y being Element of L1 st x in B2 & y in B2 holds
sup {x,y} in B2let x,
y be
Element of
L1;
( x in B2 & y in B2 implies sup {x,y} in B2 )assume that A18:
x in B2
and A19:
y in B2
;
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;
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;
( 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
;
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
;
( b in B2 & x <= b & b << y )
b in B0
by A27;
hence
b in B2
by A25;
( 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;
b << y
u is
open
by A27, YELLOW_8:10;
hence
b << y
by A9, A28, WAYBEL14:26, WAYBEL_8:8;
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; verum