:: deftheorem Def73 defines AddFormulaTo FOMODEL4:def 73 :
for X being set
for S being Language
for D being RuleSet of S
for phi being Element of AllFormulasOf S holds
( ( not xnot phi is X,D -provable implies (D,phi) AddFormulaTo X = X \/ {phi} ) & ( xnot phi is X,D -provable implies (D,phi) AddFormulaTo X = X \/ {(xnot phi)} ) );