thus x `1 is place of PTN ; :: thesis: verum