set N = TheNorSymbOf S;
set phi = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2;
set x1 = xnot phi1;
set x2 = xnot phi2;
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)];
{} /\ S is S -sequents-like ;
then reconsider SQe = {} as S -sequents-like set ;
[{(xnot phi1),(xnot phi2)},((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)] is 1 + 1,SQe \/ SQe,({(R#0 S)} \/ {(R#0 S)}) \/ {(R#6 S)} -derivable by Lm46;
then {[{(xnot phi1),(xnot phi2)},((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]} is {} ,{(R#0 S)} \/ {(R#6 S)} -derivable by Lm12;
hence for b₁ being set st b₁ = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 holds
b₁ is {(xnot phi1),(xnot phi2)},{(R#0 S)} \/ {(R#6 S)} -provable ; :: thesis: verum