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

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