let R be Relation; :: thesis: for x being set st x in R holds
x `2 in Im R,(x `1 )
let x be set ; :: thesis: ( x in R implies x `2 in Im R,(x `1 ) )
assume Z: x in R ; :: thesis: x `2 in Im R,(x `1 )
then x `2 in { (I `2 ) where I is Element of R : I `1 = x `1 } ;
hence x `2 in Im R,(x `1 ) by Z, Th92; :: thesis: verum