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

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

hence
L is with_suprema
by YELLOW_0:20; :: thesis: verumlet 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

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}

end;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

then reconsider X = { x where x is Element of L : ( x >= a & x >= b ) } as Subset of L ;
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;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

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

end;assume A6: x in {a,b} ; :: thesis: x <= c

x is_<=_than X

proof

hence
x <= c
by A4; :: thesis: verum
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;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

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

c <= y

hence
ex_sup_of {a,b},L
by A5, YELLOW_0:15; :: thesis: verumc <= 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;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