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 b1 being set st b1 = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 holds
b1 is {(xnot phi1),(xnot phi2)},{(R#0 S)} \/ {(R#6 S)} -provable
; verum