set AF = AllFormulasOf S;
reconsider phi11 = phi1, phi22 = phi2 as Element of AllFormulasOf S by FOMODEL2:16;
reconsider Phi = {phi22} as finite Subset of (AllFormulasOf S) ;
[(Phi \/ {phi1}),phi1] is 1, {} ,{(R#0 S)} -derivable ;
hence for b₁ being object st b₁ = [{phi1,phi2},phi1] holds
b₁ is 1, {} ,{(R#0 S)} -derivable ; :: thesis: verum