let L be complete continuous LATTICE; :: thesis: for S being non empty Poset st S is_a_retract_of L holds
S is continuous
let S be non empty Poset; :: thesis: ( S is_a_retract_of L implies S is continuous )
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 continuous
reconsider g = f as directed-sups-preserving projection Function of L,L by A1, Th11, Th13;
A2: Image g is continuous LATTICE by WAYBEL15:15;
Image g = RelStr(# the carrier of S, the InternalRel of S #) by A1, Th12;
hence S is continuous by A2, YELLOW12:15; :: thesis: verum