theorem Th20: :: REWRITE1:20

for R being Relation
for a, b being object holds
( R reduces a,b iff ( a = b or [a,b] in R [*] ) )