set N = TheNorSymbOf S;
set psi1 = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2;
set psi2 = (<*(TheNorSymbOf S)*> ^ phi2) ^ phi1;
set Sq = [H,((<*(TheNorSymbOf S)*> ^ phi2) ^ phi1)];
set y = [H,((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)];
set SQ = {[H,((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]};
set Q = S -sequents ;
reconsider seqt = [H,((<*(TheNorSymbOf S)*> ^ phi2) ^ phi1)] as Element of S -sequents by Def2;
reconsider Seqts = {[H,((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]} as Element of bool (S -sequents) by Def3;
( {[H,((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]} \ {[H,((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]} = {} & ([H,((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)] `1) \+\ H = {} & ([H,((<*(TheNorSymbOf S)*> ^ phi2) ^ phi1)] `1) \+\ H = {} & ([H,((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)] `2) \+\ ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) = {} & ([H,((<*(TheNorSymbOf S)*> ^ phi2) ^ phi1)] `2) \+\ ((<*(TheNorSymbOf S)*> ^ phi2) ^ phi1) = {} ) ;
then ( [H,((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)] in {[H,((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]} & [H,((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)] `1 = H & [H,((<*(TheNorSymbOf S)*> ^ phi2) ^ phi1)] `1 = H & [H,((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)] `2 = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 & [H,((<*(TheNorSymbOf S)*> ^ phi2) ^ phi1)] `2 = (<*(TheNorSymbOf S)*> ^ phi2) ^ phi1 ) by FOMODEL0:29;
then seqt Rule7 Seqts ;
then [Seqts,seqt] in P#7 S by Def44;
then [H,((<*(TheNorSymbOf S)*> ^ phi2) ^ phi1)] in (R#7 S) . {[H,((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]} by Th3;
hence for b₁ being object st b₁ = [H,((<*(TheNorSymbOf S)*> ^ phi2) ^ phi1)] holds
b₁ is 1,{[H,((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]},{(R#7 S)} -derivable by Lm7; :: thesis: verum