let R be non empty Relation; for x being object holds Im (R,x) = { (I `2) where I is Element of R : I `1 = x }
let x be object ; 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 }
XBOOLE_0:def 10 { (I `2) where I is Element of R : I `1 = x } c= Im (R,x)
let z be object ; TARSKI:def 3 ( 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 }
; z in Im (R,x)
then consider I being Element of R such that
A4:
z = I `2
and
A5:
I `1 = x
;
A6:
I = [(I `1),(I `2)]
by Th15;
x in {x}
by TARSKI:def 1;
hence
z in Im (R,x)
by A4, A5, A6, RELAT_1:def 13; verum