theorem Th20: :: YELLOW_0:20

for L being antisymmetric RelStr holds
( L is with_suprema iff for a, b being Element of L holds ex_sup_of {a,b},L )