let R be Relation; :: thesis: R c= [:(field R),(field R):]
let y be set ; :: according to RELAT_1:def 3 :: thesis: for b₁ being set holds
( not [y,b₁] in R or [y,b₁] in [:(field R),(field R):] )
let z be set ; :: thesis: ( not [y,z] in R or [y,z] in [:(field R),(field R):] )
assume [y,z] in R ; :: thesis: [y,z] in [:(field R),(field R):]
then ( y in field R & z in field R ) by RELAT_1:30;
hence [y,z] in [:(field R),(field R):] by ZFMISC_1:106; :: thesis: verum