let T be non empty up-complete Poset; :: thesis: for S being non empty Poset
for f being Function of T,T st f is_a_retraction_of T,S holds
( f is directed-sups-preserving & f is projection )
let S be non empty Poset; :: thesis: for f being Function of T,T st f is_a_retraction_of T,S holds
( f is directed-sups-preserving & f is projection )
let f be Function of T,T; :: thesis: ( f is_a_retraction_of T,S implies ( f is directed-sups-preserving & f is projection ) )
assume A1: f is_a_retraction_of T,S ; :: thesis: ( f is directed-sups-preserving & f is projection )
then reconsider g = f as directed-sups-preserving Function of T,S ;
f is idempotent by A1, Th11;
then A2: f = f * f by QUANTAL1:def 9
.= (f | (rng f)) * f by FUNCT_4:2
.= (f | the carrier of S) * f by A1, Th8, Th10
.= (id S) * f by A1
.= (id the carrier of S) * g ;
A3: S is non empty full directed-sups-inheriting SubRelStr of T by A1;
then A4: incl (S,T) is directed-sups-preserving by WAYBEL21:10;
the carrier of S c= the carrier of T by A3, YELLOW_0:def 13;
then A5: incl (S,T) = id the carrier of S by YELLOW_9:def 1;
hence f is directed-sups-preserving by A2, A4, WAYBEL20:28; :: thesis: f is projection
f is idempotent directed-sups-preserving Function of T,T by A1, A2, A4, A5, Th11, WAYBEL20:28;
hence f is projection ; :: thesis: verum