let L be complete continuous LATTICE; :: thesis: for S being non empty Poset st S is_an_UPS_retract_of L holds
S is continuous
let S be non empty Poset; :: thesis: ( S is_an_UPS_retract_of L implies S is continuous )
given f being Function of L,S such that A1: f is_an_UPS_retraction_of L,S ; :: according to YELLOW16:def 4 :: thesis: S is continuous
consider h being directed-sups-preserving projection Function of L,L such that
A2: h is_a_retraction_of L, Image h and
A3: S, Image h are_isomorphic by A1, Th18;
Image h is_a_retract_of L by A2;
then Image h is continuous by Th21;
hence S is continuous by A3, WAYBEL15:9, WAYBEL_1:6; :: thesis: verum