let T, S be non empty Poset; 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; ( 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
; 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; verum