theorem :: ORDERS_1:72

for R being Relation
for X being set st R is_reflexive_in X holds
R |_2 X is reflexive by Lm8;