let L be antisymmetric RelStr ; :: thesis: for a, b, c being Element of L holds
( c = a "\/" b & ex_sup_of {a,b},L iff ( c >= a & c >= b & ( for d being Element of L st d >= a & d >= b holds
c <= d ) ) )
let a, b, c be Element of L; :: thesis: ( c = a "\/" b & ex_sup_of {a,b},L iff ( c >= a & c >= b & ( for d being Element of L st d >= a & d >= b holds
c <= d ) ) )

hereby :: thesis: ( c >= a & c >= b & ( for d being Element of L st d >= a & d >= b holds
c <= d ) implies ( c = a "\/" b & ex_sup_of {a,b},L ) )

assume that
A1: c = a "\/" b and
A2: ex_sup_of {a,b},L ; :: thesis: ( c >= a & c >= b & ( for d being Element of L st d >= a & d >= b holds
c <= d ) )
consider c1 being Element of L such that
A3: {a,b} is_<=_than c1 and
A4: for d being Element of L st {a,b} is_<=_than d holds
c1 <= d by A2, Th15;

A5: now

let d be Element of L; :: thesis: ( a <= d & b <= d implies c1 <= d )
assume ( a <= d & b <= d ) ; :: thesis: c1 <= d
then {a,b} is_<=_than d by Th8;
hence c1 <= d by A4; :: thesis: verum

end;

( a <= c1 & b <= c1 ) by A3, Th8;
hence ( c >= a & c >= b & ( for d being Element of L st d >= a & d >= b holds
c <= d ) ) by A1, A5, LATTICE3:def 13; :: thesis: verum

end;

assume A6: ( c >= a & c >= b & ( for d being Element of L st d >= a & d >= b holds
c <= d ) ) ; :: thesis: ( c = a "\/" b & ex_sup_of {a,b},L )
hence c = a "\/" b by LATTICE3:def 13; :: thesis: ex_sup_of {a,b},L

now

take c = c; :: thesis: ( c is_>=_than {a,b} & ( for d being Element of L st d is_>=_than {a,b} holds
c <= d ) )
thus c is_>=_than {a,b} by A6, Th8; :: thesis: for d being Element of L st d is_>=_than {a,b} holds
c <= d
let d be Element of L; :: thesis: ( d is_>=_than {a,b} implies c <= d )
assume d is_>=_than {a,b} ; :: thesis: c <= d
then ( d >= a & d >= b ) by Th8;
hence c <= d by A6; :: thesis: verum

end;

hence ex_sup_of {a,b},L by Th15; :: thesis: verum