theorem Th6: :: WAYBEL20:6

for S being non empty antisymmetric RelStr st ex_sup_of {} ,S holds
S is lower-bounded