let R be Relation; :: thesis: for x being object st x in R holds
x `2 in Im (R,(x `1))
let x be object ; :: thesis: ( x in R implies x `2 in Im (R,(x `1)) )
assume A1: 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 A1, Th71; :: thesis: verum