theorem Th17: :: WAYBEL34:17

for W being with_non-empty_element set holds the carrier of (W -INF_category) = the carrier of (W -SUP_category)