theorem :: YELLOW_5:28

for L being transitive antisymmetric with_infima lower-bounded RelStr
for a being Element of L holds a misses Bottom L by Th25;