set N = TheNorSymbOf S;
set v1 = I -TruthEval phi;
set psi = xnot phi;
(I -TruthEval (xnot phi)) \+\ ((I -TruthEval phi) 'nor' (I -TruthEval phi)) = {} ;
hence for b₁ being set st b₁ = (I -TruthEval (xnot phi)) \+\ ('not' (I -TruthEval phi)) holds
b₁ is empty ; :: thesis: verum