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 A1: [y,z] in R ; :: thesis: [y,z] in [:(field R),(field R):]
then A2: z in field R by RELAT_1:15;
y in field R by A1, RELAT_1:15;
hence [y,z] in [:(field R),(field R):] by A2, ZFMISC_1:87; :: thesis: verum