let R be Relation; :: thesis: for X being set st R is_reflexive_in X holds
R |_2 X is reflexive
let X be set ; :: thesis: ( R is_reflexive_in X implies R |_2 X is reflexive )
assume A1: for x being object st x in X holds
[x,x] in R ; :: according to RELAT_2:def 1 :: thesis: R |_2 X is reflexive
let x be object ; :: according to RELAT_2:def 1,RELAT_2:def 9 :: thesis: ( not x in field (R |_2 X) or [x,x] in R |_2 X )
assume A2: x in field (R |_2 X) ; :: thesis: [x,x] in R |_2 X
then x in X by WELLORD1:12;
then A3: [x,x] in [:X,X:] by ZFMISC_1:87;
[x,x] in R by A1, A2, WELLORD1:12;
hence [x,x] in R |_2 X by A3, XBOOLE_0:def 4; :: thesis: verum