set Q = S -sequents ;
set x1 = xnot phi1;
set x2 = xnot phi2;
set N = TheNorSymbOf S;
set prem = {(xnot phi1),(xnot phi2)};
set sq = [{(xnot phi1),(xnot phi2)},((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)];
set sq1 = [{(xnot phi1),(xnot phi2)},(xnot phi1)];
set sq2 = [{(xnot phi1),(xnot phi2)},(xnot phi2)];
set SQ = {[{(xnot phi1),(xnot phi2)},(xnot phi1)],[{(xnot phi1),(xnot phi2)},(xnot phi2)]};
reconsider seqt = [{(xnot phi1),(xnot phi2)},((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)] as Element of S -sequents by Def2;
reconsider Seqts = {[{(xnot phi1),(xnot phi2)},(xnot phi1)],[{(xnot phi1),(xnot phi2)},(xnot phi2)]} as Element of bool (S -sequents) by Def3;
( {[{(xnot phi1),(xnot phi2)},(xnot phi1)]} \ Seqts = {} & {[{(xnot phi1),(xnot phi2)},(xnot phi2)]} \ Seqts = {} & ([{(xnot phi1),(xnot phi2)},(xnot phi1)] `1) \+\ {(xnot phi1),(xnot phi2)} = {} & ([{(xnot phi1),(xnot phi2)},(xnot phi2)] `1) \+\ {(xnot phi1),(xnot phi2)} = {} & ([{(xnot phi1),(xnot phi2)},((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)] `1) \+\ {(xnot phi1),(xnot phi2)} = {} & ([{(xnot phi1),(xnot phi2)},((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)] `1) \+\ {(xnot phi1),(xnot phi2)} = {} & ([{(xnot phi1),(xnot phi2)},(xnot phi1)] `2) \+\ (xnot phi1) = {} & ([{(xnot phi1),(xnot phi2)},(xnot phi2)] `2) \+\ (xnot phi2) = {} & ([{(xnot phi1),(xnot phi2)},((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)] `2) \+\ ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) = {} ) ;
then ( [{(xnot phi1),(xnot phi2)},(xnot phi1)] in Seqts & [{(xnot phi1),(xnot phi2)},(xnot phi2)] in Seqts & [{(xnot phi1),(xnot phi2)},(xnot phi1)] `1 = {(xnot phi1),(xnot phi2)} & [{(xnot phi1),(xnot phi2)},(xnot phi2)] `1 = {(xnot phi1),(xnot phi2)} & [{(xnot phi1),(xnot phi2)},((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)] `1 = {(xnot phi1),(xnot phi2)} & [{(xnot phi1),(xnot phi2)},(xnot phi1)] `2 = xnot phi1 & [{(xnot phi1),(xnot phi2)},(xnot phi2)] `2 = xnot phi2 & [{(xnot phi1),(xnot phi2)},((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)] `2 = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 ) by FOMODEL0:29;
then seqt Rule6 Seqts ;
then [Seqts,seqt] in P#6 S by Def43;
then seqt in (R#6 S) . Seqts by Lm27;
hence for b₁ being object st b₁ = [{(xnot phi1),(xnot phi2)},((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)] holds
b₁ is 1,{[{(xnot phi1),(xnot phi2)},(xnot phi1)],[{(xnot phi1),(xnot phi2)},(xnot phi2)]},{(R#6 S)} -derivable by Lm7; :: thesis: verum