theorem Th4: :: WAYBEL_3:4

for L being non empty reflexive antisymmetric lower-bounded RelStr
for x being Element of L holds Bottom L << x