theorem Th15: :: YELLOW_0:15

for L being antisymmetric RelStr
for X being set holds
( ex_sup_of X,L iff ex a being Element of L st
( X is_<=_than a & ( for b being Element of L st X is_<=_than b holds
a <= b ) ) )