set AF = AllFormulasOf S;
set E = TheEqSymbOf S;
set allpremises = {phi,((<*(TheEqSymbOf S)*> ^ t1) ^ t2)};
set IT = [{phi,((<*(TheEqSymbOf S)*> ^ t1) ^ t2)},((<*(TheEqSymbOf S)*> ^ t) ^ t2)];
reconsider phii = phi as Element of AllFormulasOf S by FOMODEL2:16;
reconsider premises = {phii} as finite Subset of (AllFormulasOf S) ;
[(premises \/ {((<*(TheEqSymbOf S)*> ^ t1) ^ t2)}),((<*(TheEqSymbOf S)*> ^ t) ^ t2)] is 1,{[premises,((<*(TheEqSymbOf S)*> ^ t) ^ t1)]},{(R3a S)} -derivable ;
hence for b₁ being set st b₁ = [{phi,((<*(TheEqSymbOf S)*> ^ t1) ^ t2)},((<*(TheEqSymbOf S)*> ^ t) ^ t2)] holds
b₁ is 1,{[{phi},((<*(TheEqSymbOf S)*> ^ t) ^ t1)]},{(R3a S)} -derivable by ENUMSET1:1; :: thesis: verum