let X be set ; for S being Language
for D being RuleSet of S
for num being sequence of (AllFormulasOf S) st rng num = AllFormulasOf S holds
(D,num) CompletionOf X is S -covering
let S be Language; for D being RuleSet of S
for num being sequence of (AllFormulasOf S) st rng num = AllFormulasOf S holds
(D,num) CompletionOf X is S -covering
let D be RuleSet of S; for num being sequence of (AllFormulasOf S) st rng num = AllFormulasOf S holds
(D,num) CompletionOf X is S -covering
set FF = AllFormulasOf S;
let num be sequence of (AllFormulasOf S); ( 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 A1:
rng num = AllFormulasOf S
; (D,num) CompletionOf X is S -covering
reconsider ff = (D,num) AddFormulasTo X as sequence of (rng ((D,num) AddFormulasTo X)) by FUNCT_2:6;
hereby FOMODEL2:def 40 verum
let phi be
wff string of
S;
( 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
object such that A2:
(
x in dom num &
num . x = phii )
by FUNCT_1:def 3, A1;
reconsider mm =
x as
Element of
NAT by A2;
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 Def74;
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 A2, Def73;
then A3:
(
{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;
hence
(
phi in (
D,
num)
CompletionOf X or
xnot phi in (
D,
num)
CompletionOf X )
by ZFMISC_1:31, A3, XBOOLE_1:1;
verum
end;