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

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

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

proof

let s be set ; :: 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 set such that
A1: ( [v,s] in R1 & v in {z} ) by RELAT_1:def 13;
thus s in Im (R2,z) by Z1, A1, RELAT_1:def 13; :: thesis: verum

end;

end;

assume Z2: for z being set holds Im (R1,z) c= Im (R2,z) ; :: thesis: R1 c= R2
let a, b be set ; :: 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 Z2, RELAT_1:169;
hence [a,b] in R2 by RELAT_1:169; :: thesis: verum