let S, T be non empty Poset; :: thesis: for f being Function st f is_a_retraction_of T,S holds
f * (incl (S,T)) = id S
let f be Function; :: thesis: ( f is_a_retraction_of T,S implies f * (incl (S,T)) = id S )
assume that
f is directed-sups-preserving Function of T,S and
A1: f | the carrier of S = id S and
A2: S is full directed-sups-inheriting SubRelStr of T ; :: according to YELLOW16:def 1 :: thesis: f * (incl (S,T)) = id S
the carrier of S c= the carrier of T by A2, YELLOW_0:def 13;
hence f * (incl (S,T)) = f * (id the carrier of S) by YELLOW_9:def 1
.= id S by A1, RELAT_1:65 ;
:: thesis: verum