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
let Y be non empty finite Subset of C; :: thesis: "\/" Y,L in Y
defpred S₁[ set ] means ( "\/" $1,L in $1 & ex_sup_of $1,L );
A2: for x being Element of C holds S₁[{x}]

proof

let x be Element of C; :: thesis: S₁[{x}]
"\/" {x},L = x by YELLOW_0:39;
hence S₁[{x}] by TARSKI:def 1, YELLOW_0:38; :: thesis: verum

end;

A3: for B1, B2 being non empty Element of Fin C st S₁[B1] & S₁[B2] holds
S₁[B1 \/ B2]

proof

let B1, B2 be non empty Element of Fin C; :: thesis: ( S₁[B1] & S₁[B2] implies S₁[B1 \/ B2] )
assume A4: ( S₁[B1] & S₁[B2] ) ; :: thesis: S₁[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, A4;
then A5: ( ("\/" 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 A4, YELLOW_2:3;
hence S₁[B1 \/ B2] by A4, A5, XBOOLE_0:def 3, YELLOW_2:3; :: thesis: verum

end;

A6: for B being non empty Element of Fin C holds S₁[B] from SETWISEO:sch 3(A2, A3);
Y in Fin C by FINSUB_1:def 5;
hence "\/" Y,L in Y by A6; :: thesis: verum