theorem Th5: :: WAYBEL20:5

for S being non empty antisymmetric RelStr st ex_inf_of {} ,S holds
S is upper-bounded