let R be Relation; :: thesis: R |_2 (field R) = R
let x, y be object ; :: according to RELAT_1:def 2 :: 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:15;
then [x,y] in [:(field R),(field R):] by ZFMISC_1:87;
hence [x,y] in R |_2 (field R) by A1, XBOOLE_0:def 4; :: thesis: verum