let L be non empty complete Poset; :: thesis: for S being non empty Poset st S is_a_retract_of L holds
S is complete
let S be non empty Poset; :: thesis: ( S is_a_retract_of L implies S is 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 complete
reconsider f = f as directed-sups-preserving projection Function of L,L by A1, Th14, Th16;
A2: Image f is complete by YELLOW_2:37;
RelStr(# the carrier of S,the InternalRel of S #) = Image f by A1, Th15;
hence S is complete by A2, YELLOW_0:3; :: thesis: verum