let S be Language; :: thesis: for X being functional set
for D2 being 2 -ranked RuleSet of S st X is finite & AllFormulasOf S is countable & 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 ; :: thesis: for D2 being 2 -ranked RuleSet of S st X is finite & AllFormulasOf S is countable & 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; :: thesis: ( X is finite & AllFormulasOf S is countable & 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 SS = AllSymbolsOf S;
set L = LettersOf S;
set strings = ((AllSymbolsOf S) *) \ {{}};
set FF = AllFormulasOf S;
set no = SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}));
assume X is finite ; :: thesis: ( not AllFormulasOf S is countable 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 XS = X /\ (((AllSymbolsOf S) *) \ {{}}) as finite FinSequence-membered set ;
SymbolsOf XS is finite ;
then A1: (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite ;
assume ( AllFormulasOf S is countable & X is D2 -consistent & D2 is isotone ) ; :: thesis: ex U being non empty countable set ex I being Element of U -InterpretersOf S st X is I -satisfied
hence ex U being non empty countable set ex I being Element of U -InterpretersOf S st X is I -satisfied by A1, Lm75; :: thesis: verum