let L be lower-bounded sup-Semilattice; :: thesis: for B being Subset of L st B is infinite holds
card B = card ()

let B be Subset of L; :: thesis: ( B is infinite implies card B = card () )
defpred S1[ Function, set ] means \$2 = "\/" ((rng \$1),L);
assume A1: B is infinite ; :: thesis: card B = card ()
then reconsider B1 = B as non empty Subset of L ;
A2: for p being Element of B1 * ex u being Element of finsups B1 st S1[p,u]
proof
let p be Element of B1 * ; :: thesis: ex u being Element of finsups B1 st S1[p,u]
A3: rng p c= the carrier of L by XBOOLE_1:1;
now :: thesis: ex_sup_of rng p,Lend;
then "\/" ((rng p),L) in { ("\/" (Y,L)) where Y is finite Subset of B1 : ex_sup_of Y,L } ;
then reconsider u = "\/" ((rng p),L) as Element of finsups B1 by WAYBEL_0:def 27;
take u ; :: thesis: S1[p,u]
thus S1[p,u] ; :: thesis: verum
end;
consider f being Function of (B1 *),(finsups B1) such that
A4: for p being Element of B1 * holds S1[p,f . p] from B c= finsups B
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in B or z in finsups B )
assume A5: z in B ; :: thesis:
then reconsider z1 = z as Element of L ;
A6: {z1} c= B by ;
( ex_sup_of {z1},L & z = sup {z1} ) by ;
then z1 in { ("\/" (Y,L)) where Y is finite Subset of B : ex_sup_of Y,L } by A6;
hence z in finsups B by WAYBEL_0:def 27; :: thesis: verum
end;
then A7: card B c= card () by CARD_1:11;
A8: dom f = B1 * by FUNCT_2:def 1;
finsups B c= rng f
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in finsups B or z in rng f )
assume z in finsups B ; :: thesis: z in rng f
then z in { ("\/" (Y,L)) where Y is finite Subset of B : ex_sup_of Y,L } by WAYBEL_0:def 27;
then consider Y being finite Subset of B such that
A9: z = "\/" (Y,L) and
ex_sup_of Y,L ;
consider p being FinSequence such that
A10: rng p = Y by FINSEQ_1:52;
reconsider p = p as FinSequence of B1 by ;
reconsider p1 = p as Element of B1 * by FINSEQ_1:def 11;
f . p1 = "\/" ((rng p1),L) by A4;
hence z in rng f by ; :: thesis: verum
end;
then card (finsups B1) c= card (B1 *) by ;
then card (finsups B1) c= card B1 by ;
hence card B = card () by A7; :: thesis: verum