set N = TheNorSymbOf S;
set psi1 = xnot phi1;
set psi2 = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2;
set Sq = [H,((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)];
set Sq1 = [(H \/ {phi1}),((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)];
set Sq2 = [(H \/ {phi1}),phi1];
set SQ = {} null S;
set goal = [(H null (phi1 ^ phi2)),(xnot phi1)];
[(H null (phi1 ^ phi2)),(xnot phi1)] is 1 + 1,({} null S) \/ {[H,((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]},({(R#0 S)} \/ {(R#1 S)}) \/ {(R#8 S)} -derivable by Lm46;
hence [(H null phi2),(xnot phi1)] is 2,{[H,((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]},({(R#0 S)} \/ {(R#1 S)}) \/ {(R#8 S)} -derivable ; :: thesis: verum