let R be non empty Relation; :: thesis: for x being set holds Im (R,x) = { (I `2) where I is Element of R : I `1 = x }
let x be set ; :: thesis: Im (R,x) = { (I `2) where I is Element of R : I `1 = x }
set X = { (I `2) where I is Element of R : I `1 = x } ;
thus Im (R,x) c= { (I `2) where I is Element of R : I `1 = x } :: according to XBOOLE_0:def 10 :: thesis: { (I `2) where I is Element of R : I `1 = x } c= Im (R,x)

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in Im (R,x) or z in { (I `2) where I is Element of R : I `1 = x } )
assume z in Im (R,x) ; :: thesis: z in { (I `2) where I is Element of R : I `1 = x }
then consider y being set such that
W1: [y,z] in R and
W2: y in {x} by RELAT_1:def 13;
A: y = x by W2, TARSKI:def 1;
( y = [y,z] `1 & z = [y,z] `2 ) by Def1, Def2;
hence z in { (I `2) where I is Element of R : I `1 = x } by W1, A; :: thesis: verum

end;

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in { (I `2) where I is Element of R : I `1 = x } or z in Im (R,x) )
assume z in { (I `2) where I is Element of R : I `1 = x } ; :: thesis: z in Im (R,x)
then consider I being Element of R such that
W1: z = I `2 and
W2: I `1 = x ;
A: I = [(I `1),(I `2)] by Th23;
x in {x} by TARSKI:def 1;
hence z in Im (R,x) by W1, W2, A, RELAT_1:def 13; :: thesis: verum