let L1 be lower-bounded continuous sup-Semilattice; :: thesis: for T1 being Scott TopAugmentation of L1
for T2 being correct Lawson TopAugmentation of L1 holds weight T1 c= weight T2
let T1 be Scott TopAugmentation of L1; :: thesis: for T2 being correct Lawson TopAugmentation of L1 holds weight T1 c= weight T2
let T2 be correct Lawson TopAugmentation of L1; :: thesis: weight T1 c= weight T2
consider B1 being Basis of T2 such that
A1: card B1 = weight T2 by WAYBEL23:74;
defpred S₁[ object , object ] means ex y being Subset of T2 st
( y = $1 & $2 = uparrow y );
A2: for x being object st x in B1 holds
ex z being object st S₁[x,z]

proof

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

end;

consider f being Function such that
A3: dom f = B1 and
A4: for x being object st x in B1 holds
S₁[x,f . x] from CLASSES1:sch 1(A2);
{ (uparrow V) where V is Subset of T2 : V in B1 } c= rng f

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { (uparrow V) where V is Subset of T2 : V in B1 } or z in rng f )
assume z in { (uparrow V) where V is Subset of T2 : V in B1 } ; :: thesis: z in rng f
then consider V being Subset of T2 such that
A5: z = uparrow V and
A6: V in B1 ;
ex V1 being Subset of T2 st
( V1 = V & f . V = uparrow V1 ) by A4, A6;
hence z in rng f by A3, A5, A6, FUNCT_1:def 3; :: thesis: verum

end;

then A7: card { (uparrow V) where V is Subset of T2 : V in B1 } c= card B1 by A3, CARD_1:12;
{ (uparrow V) where V is Subset of T2 : V in B1 } is Basis of T1 by Th10;
then card { (uparrow V) where V is Subset of T2 : V in B1 } in { (card B2) where B2 is Basis of T1 : verum } ;
then meet { (card B2) where B2 is Basis of T1 : verum } c= card { (uparrow V) where V is Subset of T2 : V in B1 } by SETFAM_1:3;
then meet { (card B2) where B2 is Basis of T1 : verum } c= card B1 by A7;
hence weight T1 c= weight T2 by A1, WAYBEL23:def 5; :: thesis: verum