let L be non empty up-complete Poset; :: thesis: for S being non empty Poset st S is_a_retract_of L holds
S is up-complete
let S be non empty Poset; :: thesis: ( S is_a_retract_of L implies S is up-complete )
given f being Function of L,S such that A1: f is_a_retraction_of L,S ; :: according to YELLOW16:def 3 :: thesis: S is up-complete
S is non empty full directed-sups-inheriting SubRelStr of L by A1;
hence S is up-complete by Th4; :: thesis: verum