let R be Relation; :: thesis: R |_2 (field R) = R
let x be set ; :: according to RELAT_1:def 2 :: thesis: for b₁ being set holds
( ( not [x,b₁] in R |_2 (field R) or [x,b₁] in R ) & ( not [x,b₁] in R or [x,b₁] in R |_2 (field R) ) )
let y be set ; :: thesis: ( ( not [x,y] in R |_2 (field R) or [x,y] in R ) & ( not [x,y] in R or [x,y] in R |_2 (field R) ) )
thus ( [x,y] in R |_2 (field R) implies [x,y] in R ) by XBOOLE_0:def 4; :: thesis: ( not [x,y] in R or [x,y] in R |_2 (field R) )
assume A1: [x,y] in R ; :: thesis: [x,y] in R |_2 (field R)
then ( x in field R & y in field R ) by RELAT_1:30;
then [x,y] in [:(field R),(field R):] by ZFMISC_1:106;
hence [x,y] in R |_2 (field R) by A1, XBOOLE_0:def 4; :: thesis: verum