let L be antisymmetric RelStr ; :: thesis: ( L is with_suprema iff for a, b being Element of L holds ex_sup_of {a,b},L )

hereby :: thesis: ( ( for a, b being Element of L holds ex_sup_of {a,b},L ) implies L is with_suprema )

assume A1: L is with_suprema ; :: 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
ex z being Element of L st
( a <= z & b <= z & ( for z9 being Element of L st a <= z9 & b <= z9 holds
z <= z9 ) ) by A1;
hence ex_sup_of {a,b},L by Th18; :: thesis: verum

end;

assume A2: for a, b being Element of L holds ex_sup_of {a,b},L ; :: thesis: L is with_suprema
let x, y be Element of L; :: according to LATTICE3:def 10 :: thesis: ex b₁ being Element of the carrier of L st
( x <= b₁ & y <= b₁ & ( for b₂ being Element of the carrier of L holds
( not x <= b₂ or not y <= b₂ or b₁ <= b₂ ) ) )
take x "\/" y ; :: thesis: ( x <= x "\/" y & y <= x "\/" y & ( for b₁ being Element of the carrier of L holds
( not x <= b₁ or not y <= b₁ or x "\/" y <= b₁ ) ) )
ex_sup_of {x,y},L by A2;
hence ( x <= x "\/" y & y <= x "\/" y & ( for b₁ being Element of the carrier of L holds
( not x <= b₁ or not y <= b₁ or x "\/" y <= b₁ ) ) ) by Th18; :: thesis: verum