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