theorem Th15: :: REWRITE1:15

for R being Relation
for a, b being object st [a,b] in R holds
R reduces a,b