theorem Th77: :: MSAFREE4:77

for I being set
for A being ManySortedSet of I ex R being ManySortedRelation of A st
( R = I --> {} & R is terminating )