let R be Relation; R |_2 (field R) = R
let x, y be object ; RELAT_1:def 2 ( ( 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; ( not [x,y] in R or [x,y] in R |_2 (field R) )
assume A1:
[x,y] in R
; [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; verum