theorem Th12: :: REWRITE1:12

for R being Relation
for a being object holds R reduces a,a