let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in NonTerminals PeanoNat or x in {S} )
assume x in NonTerminals PeanoNat ; :: thesis: x in {S}
then consider y being Symbol of PeanoNat such that
A1: x = y and
A2: ex tnt being FinSequence st y ==> tnt by Lm11;
( y = O or y = S ) by Lm2, TARSKI:def 2;
hence x in {S} by A1, A2, Lm8, TARSKI:def 1; :: thesis: verum