let X be set ; :: thesis: for R being Relation st R is reflexive holds
R |_2 X is reflexive
let R be Relation; :: thesis: ( R is reflexive implies R |_2 X is reflexive )
assume A1: R is reflexive ; :: thesis: R |_2 X is reflexive

now

let a be set ; :: thesis: ( a in field (R |_2 X) implies [a,a] in R |_2 X )
assume a in field (R |_2 X) ; :: thesis: [a,a] in R |_2 X
then ( a in field R & a in X ) by Th19;
then ( [a,a] in R & [a,a] in [:X,X:] ) by A1, Lm1, ZFMISC_1:106;
hence [a,a] in R |_2 X by XBOOLE_0:def 4; :: thesis: verum

end;

hence R |_2 X is reflexive by Lm1; :: thesis: verum