set F = S -firstChar ;
set IT = (D,phi) AddAsWitnessTo X;
set L = LettersOf S;
set l1 = (S -firstChar) . phi;
set phi1 = head phi;
set SS = AllSymbolsOf S;
set strings = ((AllSymbolsOf S) *) \ {{}};
set FF = AllFormulasOf S;
set no = SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ (X \/ {(head phi)}));
set s2 = the Element of (LettersOf S) \ (SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ (X \/ {(head phi)})));
defpred S₁[] means ( X \/ {phi} is D -consistent & (LettersOf S) \ (SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ (X \/ {(head phi)}))) <> {} );

per cases ( S₁[] or not S₁[] ) ;

suppose A1: S₁[] ; :: thesis: (D,phi) AddAsWitnessTo X is Subset of (X \/ (AllFormulasOf S))

then reconsider Y = (LettersOf S) \ (SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ (X \/ {(head phi)}))) as non empty set ;
( the Element of (LettersOf S) \ (SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ (X \/ {(head phi)}))) in Y & Y c= LettersOf S ) ;
then reconsider l2 = the Element of (LettersOf S) \ (SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ (X \/ {(head phi)}))) as literal Element of AllSymbolsOf S ;
reconsider psi = (((S -firstChar) . phi),l2) -SymbolSubstIn (head phi) as wff string of S ;
reconsider psii = psi as Element of AllFormulasOf S by FOMODEL2:16;
(D,phi) AddAsWitnessTo X = X \/ {psii} by A1, Def66;
hence (D,phi) AddAsWitnessTo X is Subset of (X \/ (AllFormulasOf S)) by XBOOLE_1:9; :: thesis: verum

end;

suppose not S₁[] ; :: thesis: (D,phi) AddAsWitnessTo X is Subset of (X \/ (AllFormulasOf S))

then (D,phi) AddAsWitnessTo X = X null (AllFormulasOf S) by Def66;
hence (D,phi) AddAsWitnessTo X is Subset of (X \/ (AllFormulasOf S)) ; :: thesis: verum

end;

end;