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 S_{1}[ set ] means ( "\/" ($1,L) in $1 & ex_sup_of $1,L );

A2: for B1, B2 being non empty Element of Fin C st S_{1}[B1] & S_{1}[B2] holds

S_{1}[B1 \/ B2]

A5: Y in Fin C by FINSUB_1:def 5;

A6: for x being Element of C holds S_{1}[{x}]
_{1}[B]
from SETWISEO:sch 3(A6, A2);

hence "\/" (Y,L) in Y by A5; :: thesis: verum

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 S

A2: for B1, B2 being non empty Element of Fin C st S

S

proof

let Y be non empty finite Subset of C; :: thesis: "\/" (Y,L) in Y
let B1, B2 be non empty Element of Fin C; :: thesis: ( S_{1}[B1] & S_{1}[B2] implies S_{1}[B1 \/ B2] )

assume A3: ( S_{1}[B1] & S_{1}[B2] )
; :: thesis: S_{1}[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 A3, YELLOW_2:3;

hence S_{1}[B1 \/ B2]
by A3, A4, XBOOLE_0:def 3, YELLOW_2:3; :: thesis: verum

end;assume A3: ( S

( 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 A3, YELLOW_2:3;

hence S

A5: Y in Fin C by FINSUB_1:def 5;

A6: for x being Element of C holds S

proof

for B being non empty Element of Fin C holds S
let x be Element of C; :: thesis: S_{1}[{x}]

"\/" ({x},L) = x by YELLOW_0:39;

hence S_{1}[{x}]
by TARSKI:def 1, YELLOW_0:38; :: thesis: verum

end;"\/" ({x},L) = x by YELLOW_0:39;

hence S

hence "\/" (Y,L) in Y by A5; :: thesis: verum