let R be Relation; :: thesis: R c= [:(dom R),(rng R):]
let y be set ; :: according to RELAT_1:def 3 :: thesis: for b being set st [y,b] in R holds
[y,b] in [:(dom R),(rng R):]
let z be set ; :: thesis: ( [y,z] in R implies [y,z] in [:(dom R),(rng R):] )
assume [y,z] in R ; :: thesis: [y,z] in [:(dom R),(rng R):]
then ( y in dom R & z in rng R ) by Def4, Def5;
hence [y,z] in [:(dom R),(rng R):] by ZFMISC_1:106; :: thesis: verum