set N = TheNorSymbOf S;
set H1 = H \/ {phi};
set psi = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2;
set y1 = [(H \/ {phi}),phi1];
set y2 = [(H \/ {phi}),((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)];
set SQ = {[(H \/ {phi}),phi1],[(H \/ {phi}),((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]};
set Sq = [H,(xnot phi)];
set Q = S -sequents ;
reconsider seqt = [H,(xnot phi)] as Element of S -sequents by Def2;
reconsider Seqts = {[(H \/ {phi}),phi1],[(H \/ {phi}),((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]} as Element of bool (S -sequents) by Def3;
( {[(H \/ {phi}),phi1]} \ {[(H \/ {phi}),phi1],[(H \/ {phi}),((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]} = {} & {[(H \/ {phi}),((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]} \ {[(H \/ {phi}),phi1],[(H \/ {phi}),((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]} = {} & ([(H \/ {phi}),phi1] `1) \+\ (H \/ {phi}) = {} & ([(H \/ {phi}),((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)] `1) \+\ (H \/ {phi}) = {} & ([(H \/ {phi}),phi1] `2) \+\ phi1 = {} & ([(H \/ {phi}),((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)] `2) \+\ ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) = {} & ([H,(xnot phi)] `1) \+\ H = {} & ([H,(xnot phi)] `2) \+\ (xnot phi) = {} ) ;
then ( [(H \/ {phi}),phi1] in {[(H \/ {phi}),phi1],[(H \/ {phi}),((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]} & [(H \/ {phi}),((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)] in {[(H \/ {phi}),phi1],[(H \/ {phi}),((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]} & [(H \/ {phi}),phi1] `1 = H \/ {phi} & [(H \/ {phi}),((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)] `1 = H \/ {phi} & [(H \/ {phi}),phi1] `2 = phi1 & [(H \/ {phi}),((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)] `2 = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 & [H,(xnot phi)] `1 = H & [H,(xnot phi)] `2 = xnot phi ) by FOMODEL0:29;
then seqt Rule8 Seqts ;
then [Seqts,seqt] in P#8 S by Def45;
then [H,(xnot phi)] in (R#8 S) . {[(H \/ {phi}),phi1],[(H \/ {phi}),((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]} by Th3;
hence for b₁ being object st b₁ = [(H null (phi1 ^ phi2)),(xnot phi)] holds
b₁ is 1,{[(H \/ {phi}),phi1],[(H \/ {phi}),((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]},{(R#8 S)} -derivable by Lm7; :: thesis: verum