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 f is_a_retraction_of T,S ; :: thesis: f is idempotent Function of T,T
then ( f * (incl S,T) = id S & f is Function of T,S & S is SubRelStr of T ) by Def1, Th10;
hence f is idempotent Function of T,T by Th9; :: thesis: verum