theorem Th60: :: WAYBEL34:60

for L being non empty antisymmetric lower-bounded RelStr
for S being non empty full bottom-inheriting SubRelStr of L holds Bottom S = Bottom L