let A be antisymmetric with_suprema RelStr ; :: thesis: for a, b, c being Element of A holds
( c = a "\/" b iff ( c >= a & c >= b & ( for d being Element of A st d >= a & d >= b holds
c <= d ) ) )
let a, b be Element of A; :: thesis: for c being Element of A holds
( c = a "\/" b iff ( c >= a & c >= b & ( for d being Element of A st d >= a & d >= b holds
c <= d ) ) )
ex x being Element of A st
( a <= x & b <= x & ( for c being Element of A st a <= c & b <= c holds
x <= c ) ) by LATTICE3:def 10;
hence for c being Element of A holds
( c = a "\/" b iff ( c >= a & c >= b & ( for d being Element of A st d >= a & d >= b holds
c <= d ) ) ) by LATTICE3:def 13; :: thesis: verum