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 object 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 by WELLORD1:12; :: according to XBOOLE_0:def 10 :: thesis: X c= field (R |_2 X)
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in X or y in field (R |_2 X) )
assume A3: y in X ; :: thesis: y in field (R |_2 X)
then A4: [y,y] in [:X,X:] by ZFMISC_1:87;
[y,y] in R by A1, A2, A3;
then [y,y] in R |_2 X by A4, XBOOLE_0:def 4;
hence y in field (R |_2 X) by RELAT_1:15; :: thesis: verum