let L be non empty reflexive antisymmetric upper-bounded RelStr ; :: thesis: ( L is /\-complete implies L is with_suprema )
assume A1: L is /\-complete ; :: thesis: L is with_suprema

now :: thesis: for a, b being Element of L holds ex_sup_of {a,b},L

let a, b be Element of L; :: thesis: ex_sup_of {a,b},L
set X = { x where x is Element of L : ( x >= a & x >= b ) } ;
{ x where x is Element of L : ( x >= a & x >= b ) } c= the carrier of L

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { x where x is Element of L : ( x >= a & x >= b ) } or x in the carrier of L )
assume x in { x where x is Element of L : ( x >= a & x >= b ) } ; :: thesis: x in the carrier of L
then ex z being Element of L st
( x = z & z >= a & z >= b ) ;
hence x in the carrier of L ; :: thesis: verum

end;

then reconsider X = { x where x is Element of L : ( x >= a & x >= b ) } as Subset of L ;
A2: Top L >= a by YELLOW_0:45;
Top L >= b by YELLOW_0:45;
then Top L in X by A2;
then ex_inf_of X,L by A1, Th76;
then consider c being Element of L such that
A3: c is_<=_than X and
A4: for d being Element of L st d is_<=_than X holds
d <= c and
for e being Element of L st e is_<=_than X & ( for d being Element of L st d is_<=_than X holds
d <= e ) holds
e = c ;
A5: c is_>=_than {a,b}

proof

let x be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not x in {a,b} or x <= c )
assume A6: x in {a,b} ; :: thesis: x <= c
x is_<=_than X

proof

let y be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not y in X or x <= y )
assume y in X ; :: thesis: x <= y
then ex z being Element of L st
( y = z & z >= a & z >= b ) ;
hence x <= y by A6, TARSKI:def 2; :: thesis: verum

end;

hence x <= c by A4; :: thesis: verum

end;

now :: thesis: for y being Element of L st y is_>=_than {a,b} holds
c <= y

let y be Element of L; :: thesis: ( y is_>=_than {a,b} implies c <= y )
assume A7: y is_>=_than {a,b} ; :: thesis: c <= y
then A8: y >= a by YELLOW_0:8;
y >= b by A7, YELLOW_0:8;
then y in X by A8;
hence c <= y by A3; :: thesis: verum

end;

hence ex_sup_of {a,b},L by A5, YELLOW_0:15; :: thesis: verum

end;

hence L is with_suprema by YELLOW_0:20; :: thesis: verum