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

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

hence
R |_2 X is reflexive
by Lm1; :: thesis: verum[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;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