let T, S be non empty Poset; :: thesis: for f being Function of T,T st f is_a_retraction_of T,S holds
Image f = RelStr(# the carrier of S, the InternalRel of S #)
let f be Function of T,T; :: thesis: ( f is_a_retraction_of T,S implies Image f = RelStr(# the carrier of S, the InternalRel of S #) )
A1: the carrier of (Image f) = rng f by YELLOW_0:def 15;
assume A2: f is_a_retraction_of T,S ; :: thesis: Image f = RelStr(# the carrier of S, the InternalRel of S #)
thus Image f = RelStr(# the carrier of S, the InternalRel of S #) by A2, A1, Th9, YELLOW_0:57; :: thesis: verum