let R be non empty Relation; :: thesis: for x being object holds Im (R,x) = { (I `2) where I is Element of R : I `1 = x }
let x be object ; :: 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 object ; :: 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 object such that
A1: [y,z] in R and
A2: y in {x} by RELAT_1:def 13;
A3: y = x by A2, TARSKI:def 1;
( y = [y,z] `1 & z = [y,z] `2 ) ;
hence z in { (I `2) where I is Element of R : I `1 = x } by A1, A3; :: thesis: verum
end;
let z be object ; :: 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
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; :: thesis: verum