let l1 be literal Element of S; :: thesis: for phi1 being wff string of S st <*l1*> ^ phi1 in Z holds
ex l2 being literal Element of S st
( (l1,l2) -SymbolSubstIn phi1 in Z & not l2 in rng phi1 )
let phi1 be wff string of S; :: thesis: ( <*l1*> ^ phi1 in Z implies ex l2 being literal Element of S st
( (l1,l2) -SymbolSubstIn phi1 in Z & not l2 in rng phi1 ) )
set phi = <*l1*> ^ phi1;
( <*l1*> ^ phi1 = (<*l1*> ^ phi1) ^ {} & not <*l1*> ^ phi1 is 0wff ) ;
then A6: ( l1 = (S -firstChar) . (<*l1*> ^ phi1) & phi1 = head (<*l1*> ^ phi1) ) by FOMODEL2:23;
<*l1*> ^ phi1 in ExFormulasOf S ;
then reconsider phii = <*l1*> ^ phi1 as Element of ExFormulasOf S ;
consider x being object such that
A7: ( x in dom num & num . x = phii ) by A5, FUNCT_1:def 3;
reconsider mm = x as Element of NAT by A7;
reconsider MM = mm + 1 as Element of NAT by ORDINAL1:def 12;
reconsider Xm = ((D,num) addw X) . mm as functional set ;
set no = SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ ((((D,num) addw X) . mm) \/ {phi1}));
reconsider T = (((AllSymbolsOf S) *) \ {{}}) /\ {phi1} as finite FinSequence-membered Subset of {phi1} ;
reconsider t = SymbolsOf T as finite set ;
reconsider i = (LettersOf S) \ (SymbolsOf ((((D,num) addw X) . mm) /\ (((AllSymbolsOf S) *) \ {{}}))) as infinite Subset of (LettersOf S) by Th17, A2, A4;
A8: SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ ((((D,num) addw X) . mm) \/ {phi1})) = SymbolsOf (((((AllSymbolsOf S) *) \ {{}}) /\ (((D,num) addw X) . mm)) \/ ((((AllSymbolsOf S) *) \ {{}}) /\ {phi1})) by XBOOLE_1:23
.= (SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ (((D,num) addw X) . mm))) \/ (SymbolsOf T) by FOMODEL0:47 ;
then (LettersOf S) \ (SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ ((((D,num) addw X) . mm) \/ {phi1}))) = i \ t by XBOOLE_1:41;
then reconsider yes = (LettersOf S) \ (SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ ((((D,num) addw X) . mm) \/ {phi1}))) as non empty Subset of (LettersOf S) ;
set ll2 = the Element of yes;
reconsider l2 = the Element of yes as literal Element of S by TARSKI:def 3;
set psi1 = (l1,l2) -SymbolSubstIn phi1;
dom ((D,num) addw X) = NAT by FUNCT_2:def 1;
then A9: ( ((D,num) addw X) . mm in rng ((D,num) addw X) & ((D,num) addw X) . MM in rng ((D,num) addw X) ) by FUNCT_1:def 3;
then ((D,num) addw X) . mm c= X addw (D,num) by ZFMISC_1:74;
then A10: ((D,num) addw X) . mm c= Z by A3, XBOOLE_1:1;
assume <*l1*> ^ phi1 in Z ; :: thesis: ex l2 being literal Element of S st
( (l1,l2) -SymbolSubstIn phi1 in Z & not l2 in rng phi1 )
then {(<*l1*> ^ phi1)} c= Z by ZFMISC_1:31;
then (((D,num) addw X) . mm) \/ {(<*l1*> ^ phi1)} c= Z by A10, XBOOLE_1:8;
then (((D,num) addw X) . mm) \/ {(<*l1*> ^ phi1)} is D -consistent by A3;
then (((D,num) addw X) . mm) \/ {((l1,l2) -SymbolSubstIn phi1)} = (D,phii) AddAsWitnessTo (((D,num) addw X) . mm) by Def66, A6
.= ((D,num) addw X) . (mm + 1) by Def71, A7 ;
then {((l1,l2) -SymbolSubstIn phi1)} null (((D,num) addw X) . mm) c= ((D,num) addw X) . MM ;
then (l1,l2) -SymbolSubstIn phi1 in ((D,num) addw X) . MM by ZFMISC_1:31;
then A11: (l1,l2) -SymbolSubstIn phi1 in X addw (D,num) by TARSKI:def 4, A9;
take l2 ; :: thesis: ( (l1,l2) -SymbolSubstIn phi1 in Z & not l2 in rng phi1 )
thus (l1,l2) -SymbolSubstIn phi1 in Z by A3, A11; :: thesis: not l2 in rng phi1
not l2 in SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ ((((D,num) addw X) . mm) \/ {phi1})) by XBOOLE_0:def 5;
then not l2 in SymbolsOf {phi1} by A8, XBOOLE_0:def 3;
hence not l2 in rng phi1 by FOMODEL0:45; :: thesis: verum