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_{1}[ 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_{1}[p,u]

A4: for p being Element of B1 * holds S_{1}[p,f . p]
from FUNCT_2:sch 3(A2);

B c= finsups B

A8: dom f = B1 * by FUNCT_2:def 1;

finsups B c= rng f

then card (finsups B1) c= card B1 by A1, CARD_4:24;

hence card B = card (finsups B) by A7; :: thesis: verum

card B = card (finsups B)

let B be Subset of L; :: thesis: ( B is infinite implies card B = card (finsups B) )

defpred S

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

proof

consider f being Function of (B1 *),(finsups B1) such that
let p be Element of B1 * ; :: thesis: ex u being Element of finsups B1 st S_{1}[p,u]

A3: rng p c= the carrier of L by XBOOLE_1:1;

then reconsider u = "\/" ((rng p),L) as Element of finsups B1 by WAYBEL_0:def 27;

take u ; :: thesis: S_{1}[p,u]

thus S_{1}[p,u]
; :: thesis: verum

end;A3: rng p c= the carrier of L by XBOOLE_1:1;

now :: thesis: ex_sup_of rng p,L

then
"\/" ((rng p),L) in { ("\/" (Y,L)) where Y is finite Subset of B1 : ex_sup_of Y,L }
;end;

then reconsider u = "\/" ((rng p),L) as Element of finsups B1 by WAYBEL_0:def 27;

take u ; :: thesis: S

thus S

A4: for p being Element of B1 * holds S

B c= finsups B

proof

then A7:
card B c= card (finsups B)
by CARD_1:11;
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;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

A8: dom f = B1 * by FUNCT_2:def 1;

finsups B c= rng f

proof

then
card (finsups B1) c= card (B1 *)
by A8, CARD_1:12;
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;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

then card (finsups B1) c= card B1 by A1, CARD_4:24;

hence card B = card (finsups B) by A7; :: thesis: verum