theorem :: ORDERS_1:79

for R being Relation
for X being set st R is_reflexive_in X holds
R ~ is_reflexive_in X by Lm12;