theorem :: YELLOW16:24

for L being non empty complete Poset
for S being non empty Poset st S is_an_UPS_retract_of L holds
S is complete