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

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

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

assume A3:
for z being object holds Im (R1,z) c= Im (R2,z)
; :: thesis: R1 c= R2assume 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

end;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;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

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