let R1, R2 be Relation; :: thesis: ( R1 c= R2 iff for z being object holds Im (R1,z) c= Im (R2,z) )

hereby :: thesis: ( ( for z being object holds Im (R1,z) c= Im (R2,z) ) implies R1 c= R2 )

assume A1: R1 c= R2 ; :: thesis: for z being object holds Im (R1,z) c= Im (R2,z)
let z be object ; :: thesis: Im (R1,z) c= Im (R2,z)
thus Im (R1,z) c= Im (R2,z) :: thesis: verum

proof

let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in Im (R1,z) or s in Im (R2,z) )
assume s in Im (R1,z) ; :: thesis: s in Im (R2,z)
then consider v being object such that
A2: ( [v,s] in R1 & v in {z} ) by RELAT_1:def 13;
thus s in Im (R2,z) by A1, A2, RELAT_1:def 13; :: thesis: verum

end;

end;

assume A3: for z being object holds Im (R1,z) c= Im (R2,z) ; :: thesis: R1 c= R2
let a, b be object ; :: according to RELAT_1:def 3 :: thesis: ( not [a,b] in R1 or [a,b] in R2 )
assume [a,b] in R1 ; :: thesis: [a,b] in R2
then ( b in Im (R1,a) & Im (R1,a) c= Im (R2,a) ) by A3, RELAT_1:169;
hence [a,b] in R2 by RELAT_1:169; :: thesis: verum