let L be sup-Semilattice; :: thesis: for C being non empty Subset of L st ( for x, y being Element of L st x in C & y in C & not x <= y holds
y <= x ) holds
for Y being non empty finite Subset of C holds "\/" (Y,L) in Y

let C be non empty Subset of L; :: thesis: ( ( for x, y being Element of L st x in C & y in C & not x <= y holds
y <= x ) implies for Y being non empty finite Subset of C holds "\/" (Y,L) in Y )

assume A1: for x, y being Element of L st x in C & y in C & not x <= y holds
y <= x ; :: thesis: for Y being non empty finite Subset of C holds "\/" (Y,L) in Y
defpred S1[ set ] means ( "\/" (\$1,L) in \$1 & ex_sup_of \$1,L );
A2: for B1, B2 being non empty Element of Fin C st S1[B1] & S1[B2] holds
S1[B1 \/ B2]
proof
let B1, B2 be non empty Element of Fin C; :: thesis: ( S1[B1] & S1[B2] implies S1[B1 \/ B2] )
assume A3: ( S1[B1] & S1[B2] ) ; :: thesis: S1[B1 \/ B2]
( B1 c= C & B2 c= C ) by FINSUB_1:def 5;
then ( "\/" (B1,L) <= "\/" (B2,L) or "\/" (B2,L) <= "\/" (B1,L) ) by A1, A3;
then A4: ( ("\/" (B1,L)) "\/" ("\/" (B2,L)) = "\/" (B1,L) or ("\/" (B1,L)) "\/" ("\/" (B2,L)) = "\/" (B2,L) ) by YELLOW_0:24;
"\/" ((B1 \/ B2),L) = ("\/" (B1,L)) "\/" ("\/" (B2,L)) by ;
hence S1[B1 \/ B2] by ; :: thesis: verum
end;
let Y be non empty finite Subset of C; :: thesis: "\/" (Y,L) in Y
A5: Y in Fin C by FINSUB_1:def 5;
A6: for x being Element of C holds S1[{x}]
proof
let x be Element of C; :: thesis: S1[{x}]
"\/" ({x},L) = x by YELLOW_0:39;
hence S1[{x}] by ; :: thesis: verum
end;
for B being non empty Element of Fin C holds S1[B] from hence "\/" (Y,L) in Y by A5; :: thesis: verum