let R be Relation; :: thesis: for X being set st R is reflexive & X c= field R holds
field (R |_2 X) = X
let X be set ; :: thesis: ( R is reflexive & X c= field R implies field (R |_2 X) = X )
assume that
A1: for x being set st x in field R holds
[x,x] in R and
A2: X c= field R ; :: according to RELAT_2:def 1,RELAT_2:def 9 :: thesis: field (R |_2 X) = X
thus field (R |_2 X) c= X :: according to XBOOLE_0:def 10 :: thesis: X c= field (R |_2 X)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in field (R |_2 X) or y in X )
thus ( not y in field (R |_2 X) or y in X ) by WELLORD1:19; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in X or y in field (R |_2 X) )
assume y in X ; :: thesis: y in field (R |_2 X)
then ( [y,y] in R & [y,y] in [:X,X:] ) by A1, A2, ZFMISC_1:106;
then [y,y] in R |_2 X by XBOOLE_0:def 4;
hence y in field (R |_2 X) by RELAT_1:30; :: thesis: verum