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 b1 being set st b1 = [H,phi] null 1 holds
b1 is 1,{[H,(xnot (xnot phi))]},{(R#9 S)} -derivable
by Lm7; verum