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 DefSeqtLike;
reconsider Seqts = {[H,(xnot (xnot phi))]} as Element of bool (S -sequents) by DefSeqtLike2;
( (seqt `2) \+\ phi = {} & ([H,(xnot (xnot phi))] `1) \+\ H = {} & (seqt `1) \+\ H = {} & ([H,(xnot (xnot phi))] `2) \+\ (xnot (xnot phi)) = {} ) ;
then ( seqt `2 = phi & [H,(xnot (xnot phi))] `1 = H & seqt `1 = H & [H,(xnot (xnot phi))] `2 = xnot (xnot phi) ) by FOMODEL0:29;
then ( [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 by Def9;
then [Seqts,seqt] in P9 S by DefP9;
then [H,phi] in (R9 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))]},{(R9 S)} -derivable by Lm22; :: thesis: verum