let L be non empty antisymmetric lower-bounded RelStr ; :: thesis: Bottom L is co-prime
Top (L ~) is prime by Th20;
hence (Bottom L) ~ is prime by YELLOW_7:33; :: according to WAYBEL_6:def 8 :: thesis: verum