set N = TheNorSymbOf S;
set nphi = xnot phi;
set phii = xnot (xnot phi);
set y = [H,(xnot (xnot phi))];
set SQ = {[H,(xnot (xnot phi))]};
set Sq = [H,phi];
set Q = S -sequents ;
reconsider seqt = [H,phi] as Element of S -sequents by Def2;
reconsider Seqts = {[H,(xnot (xnot phi))]} as Element of bool (S -sequents) by Def3;
( [H,(xnot (xnot phi))] `1 = seqt `1 & seqt `2 = phi & [H,(xnot (xnot phi))] `2 = xnot (xnot phi) & [H,(xnot (xnot phi))] in Seqts ) by TARSKI:def 1;
then seqt Rule9 Seqts ;
then [Seqts,seqt] in P#9 S by Def46;
then [H,phi] in (R#9 S) . {[H,(xnot (xnot phi))]} by Th3;
hence for b₁ being set st b₁ = [H,phi] null 1 holds
b₁ is 1,{[H,(xnot (xnot phi))]},{(R#9 S)} -derivable by Lm7; :: thesis: verum