let S, T be non empty Poset; :: thesis: for f being Function st f is_a_retraction_of T,S holds
f is idempotent Function of T,T
let f be Function; :: thesis: ( f is_a_retraction_of T,S implies f is idempotent Function of T,T )
assume A1: f is_a_retraction_of T,S ; :: thesis: f is idempotent Function of T,T
then A2: f is Function of T,S ;
A3: S is SubRelStr of T by A1;
f * (incl (S,T)) = id S by A1, Th7;
hence f is idempotent Function of T,T by A2, A3, Th6; :: thesis: verum