theorem Th3: :: DTCONSTR:3

roots {} = {} by Lm1;