let L be lower-bounded sup-Semilattice; :: thesis: for B being Subset of L st B is infinite holds
card B = card (finsups B)
let B be Subset of L; :: thesis: ( B is infinite implies card B = card (finsups B) )
defpred S₁[ Function, set ] means $2 = "\/" ((rng $1),L);
assume A1: B is infinite ; :: thesis: card B = card (finsups B)
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 S₁[p,u]

proof

let p be Element of B1 * ; :: thesis: ex u being Element of finsups B1 st S₁[p,u]
A3: rng p c= the carrier of L by XBOOLE_1:1;

now :: thesis: ex_sup_of rng p,L

per cases ( rng p is empty or not rng p is empty ) ;

suppose rng p is empty ; :: thesis: ex_sup_of rng p,L

hence ex_sup_of rng p,L by YELLOW_0:42; :: thesis: verum

end;

suppose not rng p is empty ; :: thesis: ex_sup_of rng p,L

hence ex_sup_of rng p,L by A3, YELLOW_0:54; :: thesis: verum

end;

end;

end;

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: S₁[p,u]
thus S₁[p,u] ; :: thesis: verum

end;

consider f being Function of (B1 *),(finsups B1) such that
A4: for p being Element of B1 * holds S₁[p,f . p] from FUNCT_2:sch 3(A2);
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: z in finsups B
then reconsider z1 = z as Element of L ;
A6: {z1} c= B by A5, TARSKI:def 1;
( ex_sup_of {z1},L & z = sup {z1} ) by YELLOW_0:38, YELLOW_0:39;
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 (finsups B) 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 A10, FINSEQ_1:def 4;
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 A8, A9, A10, FUNCT_1:def 3; :: thesis: verum

end;

then card (finsups B1) c= card (B1 *) by A8, CARD_1:12;
then card (finsups B1) c= card B1 by A1, CARD_4:24;
hence card B = card (finsups B) by A7; :: thesis: verum