theorem :: YELLOW16:23

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