thus x `2 is transition of PTN ; :: thesis: verum