thus 0 = [\0 /] by INT_1:47
.= [\(log 2,1)/] by POWER:59 ; :: thesis: verum