set F = S -firstChar ;
set L = LettersOf S;
set Y = (D,phi) AddAsWitnessTo X;
set s1 = (S -firstChar) . phi;
set phi1 = head phi;
set SS = AllSymbolsOf S;
set strings = ((AllSymbolsOf S) *) \ {{}};
set no = SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ (X \/ {(head phi)}));
set s2 = the Element of (LettersOf S) \ (SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ (X \/ {(head phi)})));
set Z = {((((S -firstChar) . phi), the Element of (LettersOf S) \ (SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ (X \/ {(head phi)})))) -SymbolSubstIn (head phi))};
defpred S₁[] means ( X \/ {phi} is D -consistent & (LettersOf S) \ (SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ (X \/ {(head phi)}))) <> {} );
( ( S₁[] implies ( X null {((((S -firstChar) . phi), the Element of (LettersOf S) \ (SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ (X \/ {(head phi)})))) -SymbolSubstIn (head phi))} c= X \/ {((((S -firstChar) . phi), the Element of (LettersOf S) \ (SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ (X \/ {(head phi)})))) -SymbolSubstIn (head phi))} & (D,phi) AddAsWitnessTo X = X \/ {((((S -firstChar) . phi), the Element of (LettersOf S) \ (SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ (X \/ {(head phi)})))) -SymbolSubstIn (head phi))} ) ) & ( not S₁[] implies (D,phi) AddAsWitnessTo X = X null {((((S -firstChar) . phi), the Element of (LettersOf S) \ (SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ (X \/ {(head phi)})))) -SymbolSubstIn (head phi))} ) ) by Def66;
hence for b₁ being set st b₁ = X \ ((D,phi) AddAsWitnessTo X) holds
b₁ is empty ; :: thesis: verum