set F = S -firstChar ;
set N = TheNorSymbOf S;
set phi = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2;
set A = I -TruthEval ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2);
set A1 = I -TruthEval phi1;
set A2 = I -TruthEval phi2;
set h = head ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2);
set t = tail ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2);
set H = I -TruthEval (head ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2));
set T = I -TruthEval (tail ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2));
( phi1 = head ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) & phi2 = tail ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) ) by Th23;
hence for b₁ being set st b₁ = (I -TruthEval ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)) \+\ ((I -TruthEval phi1) 'nor' (I -TruthEval phi2)) holds
b₁ is empty ; :: thesis: verum