let T be non empty up-complete Poset; :: thesis: for S being non empty Poset
for f being Function st f is_an_UPS_retraction_of T,S holds
ex h being directed-sups-preserving projection Function of T,T st
( h is_a_retraction_of T, Image h & S, Image h are_isomorphic )
let S be non empty Poset; :: thesis: for f being Function st f is_an_UPS_retraction_of T,S holds
ex h being directed-sups-preserving projection Function of T,T st
( h is_a_retraction_of T, Image h & S, Image h are_isomorphic )
let f be Function; :: thesis: ( f is_an_UPS_retraction_of T,S implies ex h being directed-sups-preserving projection Function of T,T st
( h is_a_retraction_of T, Image h & S, Image h are_isomorphic ) )
assume A1: f is directed-sups-preserving Function of T,S ; :: according to YELLOW16:def 2 :: thesis: ( for g being directed-sups-preserving Function of S,T holds not f * g = id S or ex h being directed-sups-preserving projection Function of T,T st
( h is_a_retraction_of T, Image h & S, Image h are_isomorphic ) )
given g being directed-sups-preserving Function of S,T such that A2: f * g = id S ; :: thesis: ex h being directed-sups-preserving projection Function of T,T st
( h is_a_retraction_of T, Image h & S, Image h are_isomorphic )
reconsider f = f as directed-sups-preserving Function of T,S by A1;
consider h being projection Function of T,T such that
A3: h = g * f and
A4: h | the carrier of (Image h) = id (Image h) and
A5: S, Image h are_isomorphic by A2, Th17;
reconsider h = h as directed-sups-preserving projection Function of T,T by A3, WAYBEL20:28;
take h ; :: thesis: ( h is_a_retraction_of T, Image h & S, Image h are_isomorphic )
reconsider R = Image h as non empty Poset ;
h = corestr h by WAYBEL_1:30;
then A6: h is directed-sups-preserving Function of T,R by WAYBEL20:22;
R is full directed-sups-inheriting SubRelStr of T by Th5;
hence h is_a_retraction_of T, Image h by A4, A6; :: thesis: S, Image h are_isomorphic
thus S, Image h are_isomorphic by A5; :: thesis: verum