theorem :: YELLOW_7:34

for L being non empty antisymmetric upper-bounded RelStr holds
( (Top L) ~ = Bottom (L opp) & ~ (Bottom (L opp)) = Top L ) by Th13, YELLOW_0:43;