environ A1: not (ex a being T st PHI[a]); begin 1: now let x be T; step0: now assume step1: PHI[x]; step2: ex a being T st PHI[a] by step1; == ExI thus contradiction by A1, step2; == ContrI end; thus not PHI[x] by step0 == NI end; for a being T holds not PHI[a] by 1; == UI