theorem :: REWRITE1:19

for R being Relation
for a, b being object st R reduces a,b holds
( a in field R iff b in field R ) by Th18;