let S be Language; for D2 being 2 -ranked RuleSet of S
for X being functional set st AllFormulasOf S is countable & (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite & X is D2 -consistent & D2 is isotone holds
ex U being non empty countable set ex I being Element of U -InterpretersOf S st X is I -satisfied
let D2 be 2 -ranked RuleSet of S; for X being functional set st AllFormulasOf S is countable & (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite & X is D2 -consistent & D2 is isotone holds
ex U being non empty countable set ex I being Element of U -InterpretersOf S st X is I -satisfied
let X be functional set ; ( AllFormulasOf S is countable & (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite & X is D2 -consistent & D2 is isotone implies ex U being non empty countable set ex I being Element of U -InterpretersOf S st X is I -satisfied )
set EF = ExFormulasOf S;
set FF = AllFormulasOf S;
set G0 = R#0 S;
set G2 = R#2 S;
set G3a = R#3a S;
set G3b = R#3b S;
set G3d = R#3d S;
set G3e = R#3e S;
set G1 = R#1 S;
set G4 = R#4 S;
set G5 = R#5 S;
set G6 = R#6 S;
set G7 = R#7 S;
set G8 = R#8 S;
set L = LettersOf S;
set SS = AllSymbolsOf S;
set strings = ((AllSymbolsOf S) *) \ {{}};
set no = SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}));
set D = D2;
set AF = AtomicFormulasOf S;
set TT = AllTermsOf S;
set d = S -diagFormula ;
D2 is 1 -ranked RuleSet of S
;
then
D2 is 0 -ranked RuleSet of S
;
then reconsider D1 = D2 as 0 -ranked 1 -ranked RuleSet of S ;
assume
AllFormulasOf S is countable
; ( not (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite or not X is D2 -consistent or not D2 is isotone or ex U being non empty countable set ex I being Element of U -InterpretersOf S st X is I -satisfied )
then reconsider FFC = AllFormulasOf S as countable set ;
(AtomicFormulasOf S) \ (AllFormulasOf S) = {}
;
then reconsider AFF = AtomicFormulasOf S as Subset of FFC by XBOOLE_1:37;
( dom (S -diagFormula) = AllTermsOf S & rng (S -diagFormula) c= AtomicFormulasOf S )
by FUNCT_2:def 1, RELAT_1:def 19;
then
card (AllTermsOf S) c= card AFF
by CARD_1:10;
then reconsider TTT = AllTermsOf S as non empty countable Subset of (((AllSymbolsOf S) *) \ {{}}) by WAYBEL12:1;
consider numaa being sequence of (((AllSymbolsOf S) *) \ {{}}) such that
A1:
FFC = rng numaa
by SUPINF_2:def 8;
reconsider numa = numaa as sequence of (AllFormulasOf S) by A1, FUNCT_2:6;
(ExFormulasOf S) \ FFC = {}
;
then reconsider EFC = ExFormulasOf S as Subset of FFC by XBOOLE_1:37;
consider numee being sequence of FFC such that
A2:
EFC = rng numee
by SUPINF_2:def 8;
reconsider nume = numee as sequence of (ExFormulasOf S) by A2, FUNCT_2:6;
assume A3:
( (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite & X is D2 -consistent )
; ( not D2 is isotone or ex U being non empty countable set ex I being Element of U -InterpretersOf S st X is I -satisfied )
A4:
( R#0 S in D1 & R#1 S in D2 & R#2 S in D1 & R#4 S in D2 & R#5 S in D2 & R#6 S in D2 & R#7 S in D2 & R#8 S in D2 )
by Def62;
set X1 = X addw (D1,nume);
set X2 = (D1,numa) CompletionOf (X addw (D1,nume));
A5:
(D1,numa) CompletionOf (X addw (D1,nume)) is S -covering
by Lm69, A1;
assume A6:
D2 is isotone
; ex U being non empty countable set ex I being Element of U -InterpretersOf S st X is I -satisfied
then
X addw (D1,nume) is D2 -consistent
by Lm68, A3, A4;
then A7:
(D1,numa) CompletionOf (X addw (D1,nume)) is D2 -consistent
by Lm74, A6, A4;
then A8:
( (D1,numa) CompletionOf (X addw (D1,nume)) is S -mincover & (D1,numa) CompletionOf (X addw (D1,nume)) is D2 -expanded )
by A4, Lm52, A5;
reconsider X22 = (D1,numa) CompletionOf (X addw (D1,nume)) as D1 -expanded set by A4, Lm52, A5, A7;
reconsider P = (X22,D1) -termEq as Equivalence_Relation of TTT ;
set f = P -class ;
( dom (P -class) = TTT & rng (P -class) = Class P )
by FUNCT_2:def 1, FUNCT_2:def 3;
then
card (Class P) c= card TTT
by CARD_1:12;
then reconsider U = Class P as non empty countable set by WAYBEL12:1;
take
U
; ex I being Element of U -InterpretersOf S st X is I -satisfied
reconsider I = D1 Henkin X22 as Element of U -InterpretersOf S ;
take
I
; X is I -satisfied
A9:
( X \ (X addw (D1,nume)) = {} & (X addw (D1,nume)) \ ((D1,numa) CompletionOf (X addw (D1,nume))) = {} )
;
then A10:
( X c= X addw (D1,nume) & X addw (D1,nume) c= X22 )
by XBOOLE_1:37;
A11:
X22 is S -witnessed
by A9, XBOOLE_1:37, Th18, A3, A4, A6, A7, A2;