let L be antisymmetric RelStr ; 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; ( 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 ) ) )
assume that
A6:
( c >= a & c >= b )
and
A7:
for d being Element of L st d >= a & d >= b holds
c <= d
; ( c = a "\/" b & ex_sup_of {a,b},L )
thus
c = a "\/" b
by A6, A7, LATTICE3:def 13; ex_sup_of {a,b},L
hence
ex_sup_of {a,b},L
by Th15; verum