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

let p be Element of B1 * ; :: thesis:
A3: rng p c= the carrier of L by XBOOLE_1:1;

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

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

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume A5: z in B ; :: thesis:
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:

end;

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in finsups B ; :: thesis:
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:

end;