theorem Th42: :: YELLOW_0:42

for L being non empty antisymmetric lower-bounded RelStr holds
( ex_sup_of {} ,L & ex_inf_of the carrier of L,L )