let S be non empty Poset; :: thesis: for T being non empty up-complete Poset
for f being Function st f is_a_retraction_of T,S holds
f is_an_UPS_retraction_of T,S
let T be non empty up-complete Poset; :: thesis: for f being Function st f is_a_retraction_of T,S holds
f is_an_UPS_retraction_of T,S
let f be Function; :: thesis: ( f is_a_retraction_of T,S implies f is_an_UPS_retraction_of T,S )
assume A1: f is_a_retraction_of T,S ; :: thesis: f is_an_UPS_retraction_of T,S
hence f is directed-sups-preserving Function of T,S ; :: according to YELLOW16:def 2 :: thesis: ex g being directed-sups-preserving Function of S,T st f * g = id S
S is full directed-sups-inheriting SubRelStr of T by A1;
then reconsider g = incl (S,T) as directed-sups-preserving Function of S,T by WAYBEL21:10;
take g ; :: thesis: f * g = id S
thus f * g = id S by A1, Th7; :: thesis: verum