set Y = (D,phi) AddFormulaTo X;
set psi = xnot phi;
defpred S₁[] means xnot phi is X,D -provable ;
( ( not S₁[] implies (D,phi) AddFormulaTo X = X \/ {phi} ) & ( S₁[] implies (D,phi) AddFormulaTo X = X \/ {(xnot phi)} ) ) by Def73;
then ( X null {phi} c= (D,phi) AddFormulaTo X or X null {(xnot phi)} c= (D,phi) AddFormulaTo X ) ;
hence for b₁ being set st b₁ = X \ ((D,phi) AddFormulaTo X) holds
b₁ is empty ; :: thesis: verum