let L be non empty reflexive antisymmetric lower-bounded RelStr ; :: thesis: Bottom L is compact
thus Bottom L << Bottom L by Th4; :: according to WAYBEL_3:def 2 :: thesis: verum