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