set F = S -firstChar ;
set IT = (D,phi) AddFormulaTo X;
set FF = AllFormulasOf S;
reconsider Y = X \/ (AllFormulasOf S) as non empty set ;
reconsider XX = X null (AllFormulasOf S) as Subset of Y ;
reconsider FFF = (AllFormulasOf S) null X as non empty Subset of Y ;
( xnot phi is Element of FFF & phi is Element of FFF ) by FOMODEL2:16;
then reconsider phii = phi, psii = xnot phi as Element of Y ;
reconsider Phi = {phii}, Psi = {psii} as Subset of Y ;
defpred S₁[] means xnot phi is X,D -provable ;
( ( not S₁[] implies (D,phi) AddFormulaTo X = XX \/ Phi ) & ( S₁[] implies (D,phi) AddFormulaTo X = XX \/ Psi ) ) by Def73;
hence (D,phi) AddFormulaTo X is Subset of (X \/ (AllFormulasOf S)) ; :: thesis: verum