(1 / 2) to_power (1 / 2) < 1 to_power (1 / 2) by POWER:37;
hence (1 / 2) to_power (1 / 2) <> 1 by POWER:26; :: thesis: verum