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 b1 being Element of the carrier of L st
( x <= b1 & y <= b1 & ( for b2 being Element of the carrier of L holds
( not x <= b2 or not y <= b2 or b1 <= b2 ) ) )
take x "\/" y ; :: thesis: ( x <= x "\/" y & y <= x "\/" y & ( for b1 being Element of the carrier of L holds
( not x <= b1 or not y <= b1 or x "\/" y <= b1 ) ) )
ex_sup_of {x,y},L by A2;
hence ( x <= x "\/" y & y <= x "\/" y & ( for b1 being Element of the carrier of L holds
( not x <= b1 or not y <= b1 or x "\/" y <= b1 ) ) ) by Th18; :: thesis: verum