theorem Th13: :: YELLOW21:13

for W being with_non-empty_element set
for x being set holds
( x is Object of (W -UPS_category) iff ( x is complete LATTICE & x in POSETS W ) )