theorem Th16: :: BINARITH:16

for z1 being Tuple of 1, BOOLEAN st z1 = <*TRUE*> holds
Absval z1 = 1