let R be Relation; :: thesis: R c= [:(dom R),(rng R):]
let y be object ; :: according to RELAT_1:def 3 :: thesis: for b being object st [y,b] in R holds
[y,b] in [:(dom R),(rng R):]
let z be object ; :: 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 XTUPLE_0:def 12, XTUPLE_0:def 13;
hence [y,z] in [:(dom R),(rng R):] by ZFMISC_1:87; :: thesis: verum