theorem Th3: :: ORDERS_4:3

for L being non empty antisymmetric upper-bounded RelStr holds the carrier of L \ {(Top L)},{(Top L)} form_upper_lower_partition_of L