theorem Th20: :: WAYBEL_6:20

for L being non empty antisymmetric upper-bounded RelStr holds Top L is prime by YELLOW_0:45;