theorem Th7: :: DTCONSTR:7

( pr1 {} = {} & pr2 {} = {} )