theorem Th2: :: ABCMIZ_A:2

for x being variable holds varcl (vars x) = vars x