theorem Th22: :: YELLOW_0:22

for L being antisymmetric with_suprema RelStr
for a, b, c being Element of L holds
( c = a "\/" b iff ( c >= a & c >= b & ( for d being Element of L st d >= a & d >= b holds
c <= d ) ) )