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 :: thesis: for a being object st a in field (R |_2 X) holds
[a,a] in R |_2 X

let a be object ; :: thesis: ( a in field (R |_2 X) implies [a,a] in R |_2 X )
assume A2: a in field (R |_2 X) ; :: thesis: [a,a] in R |_2 X
then a in X by Th12;
then A3: [a,a] in [:X,X:] by ZFMISC_1:87;
a in field R by A2, Th12;
then [a,a] in R by A1, Lm1;
hence [a,a] in R |_2 X by A3, XBOOLE_0:def 4; :: thesis: verum

end;

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