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