theorem Th13: :: REWRITE1:13

for a, b being object st {} reduces a,b holds
a = b