theorem Th18: :: YELLOW_0:18

for L being 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 ) ) )