for L being non empty reflexive antisymmetric lower-bounded RelStr holds Bottom L is compact by Th4;