theorem Th15: :: BINARITH:15
for z1 being Tuple of 1, BOOLEAN st z1 = <*FALSE*> holds
Absval z1 = 0