let X be set ; :: thesis: for S being Language
for D being RuleSet of S
for num being Function of NAT,(AllFormulasOf S) st rng num = AllFormulasOf S holds
(D,num) CompletionOf X is S -covering
let S be Language; :: thesis: for D being RuleSet of S
for num being Function of NAT,(AllFormulasOf S) st rng num = AllFormulasOf S holds
(D,num) CompletionOf X is S -covering
let D be RuleSet of S; :: thesis: for num being Function of NAT,(AllFormulasOf S) st rng num = AllFormulasOf S holds
(D,num) CompletionOf X is S -covering
set FF = AllFormulasOf S;
let num be Function of NAT,(AllFormulasOf S); :: thesis: ( rng num = AllFormulasOf S implies (D,num) CompletionOf X is S -covering )
set XX = (D,num) CompletionOf X;
set f = (D,num) AddFormulasTo X;
assume BB0: rng num = AllFormulasOf S ; :: thesis: (D,num) CompletionOf X is S -covering
reconsider ff = (D,num) AddFormulasTo X as Function of NAT,(rng ((D,num) AddFormulasTo X)) by FUNCT_2:6;

hereby :: according to FOMODEL2:def 40 :: thesis: verum

let phi be wff string of S; :: thesis: ( phi in (D,num) CompletionOf X or xnot phi in (D,num) CompletionOf X )
reconsider phii = phi as Element of AllFormulasOf S by FOMODEL2:16;
consider x being set such that
C0: ( x in dom num & num . x = phii ) by BB0, FUNCT_1:def 3;
reconsider mm = x as Element of NAT by C0;
reconsider MM = mm + 1 as Element of NAT by ORDINAL1:def 12;
((D,num) AddFormulasTo X) . (mm + 1) = (D,(num . mm)) AddFormulaTo (((D,num) AddFormulasTo X) . mm) by DefAdd2;
then ( ((D,num) AddFormulasTo X) . (mm + 1) = (((D,num) AddFormulasTo X) . mm) \/ {phi} or ((D,num) AddFormulasTo X) . (mm + 1) = (((D,num) AddFormulasTo X) . mm) \/ {(xnot phi)} ) by C0, DefAdd1;
then C1: ( {phi} null (((D,num) AddFormulasTo X) . mm) c= ((D,num) AddFormulasTo X) . MM or {(xnot phi)} null (((D,num) AddFormulasTo X) . mm) c= ((D,num) AddFormulasTo X) . MM ) ;
ff . MM is Element of rng ((D,num) AddFormulasTo X) ;
then ((D,num) AddFormulasTo X) . (mm + 1) c= (D,num) CompletionOf X by ZFMISC_1:74;
then ( {phi} c= (D,num) CompletionOf X or {(xnot phi)} c= (D,num) CompletionOf X ) by C1, XBOOLE_1:1;
hence ( phi in (D,num) CompletionOf X or xnot phi in (D,num) CompletionOf X ) by ZFMISC_1:31; :: thesis: verum

end;