for L being non empty antisymmetric lower-bounded RelStr holds
( (Bottom L) ~ = Top (L opp) & ~ (Top (L opp)) = Bottom L ) by Th12, YELLOW_0:42;