let S be Language; :: thesis: for D2 being 2 -ranked RuleSet of S
for X being functional set st X is finite & AllFormulasOf S is countable & not X is D2 -inconsistent & D2 is isotone holds
ex U being non empty set ex I being Element of U -InterpretersOf S st X is I -satisfied
let D2 be 2 -ranked RuleSet of S; :: thesis: for X being functional set st X is finite & AllFormulasOf S is countable & not X is D2 -inconsistent & D2 is isotone holds
ex U being non empty set ex I being Element of U -InterpretersOf S st X is I -satisfied
let X be functional set ; :: thesis: ( X is finite & AllFormulasOf S is countable & not X is D2 -inconsistent & D2 is isotone implies ex U being non empty 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 X is D2 -inconsistent or not D2 is isotone or ex U being non empty 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 B0: not (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is finite ;
assume ( AllFormulasOf S is countable & not X is D2 -inconsistent & D2 is isotone ) ; :: thesis: ex U being non empty set ex I being Element of U -InterpretersOf S st X is I -satisfied
hence ex U being non empty set ex I being Element of U -InterpretersOf S st X is I -satisfied by B0, Lm37; :: thesis: verum