theorem Th12: :: YELLOW21:12

for W being with_non-empty_element set holds the carrier of (W -UPS_category) c= POSETS W