theorem Th19: :: YELLOW_5:19

for L being non empty antisymmetric lower-bounded RelStr
for a being Element of L st a <= Bottom L holds
a = Bottom L