set N = TheNorSymbOf S;
set psi2 = (<*(TheNorSymbOf S)*> ^ phi2) ^ phi1;
set Sq1 = [H,((<*(TheNorSymbOf S)*> ^ phi2) ^ phi1)];
set D1 = {(R#7 S)};
set D2 = {(R#7 S)};
set D3 = ({(R#0 S)} \/ {(R#1 S)}) \/ {(R#8 S)};
set goal = [(H null phi1),(xnot phi2)];
set SQ1 = {[H,((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]};
set SQ2 = {[H,((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]};
A1: ( {(R#7 S)} \/ {(R#7 S)} is isotone & ({(R#7 S)} \/ {(R#7 S)}) \/ (({(R#0 S)} \/ {(R#1 S)}) \/ {(R#8 S)}) is isotone & {[H,((<*(TheNorSymbOf S)*> ^ phi2) ^ phi1)],[H,((<*(TheNorSymbOf S)*> ^ phi2) ^ phi1)]} = {[H,((<*(TheNorSymbOf S)*> ^ phi2) ^ phi1)]} \/ {[H,((<*(TheNorSymbOf S)*> ^ phi2) ^ phi1)]} ) by ENUMSET1:1;
[(H null phi1),(xnot phi2)] is 1 + 2,{[H,((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]} \/ {[H,((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]},({(R#7 S)} \/ {(R#7 S)}) \/ (({(R#0 S)} \/ {(R#1 S)}) \/ {(R#8 S)}) -derivable by A1, Lm46;
hence for b₁ being object st b₁ = [(H null phi1),(xnot phi2)] holds
b₁ is 3,{[H,((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]},(({(R#0 S)} \/ {(R#1 S)}) \/ {(R#8 S)}) \/ {(R#7 S)} -derivable ; :: thesis: verum