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