let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Terminals PeanoNat or x in {O} )
assume x in Terminals PeanoNat ; :: thesis: x in {O}
then consider y being Symbol of PeanoNat such that
A1: ( x = y & ( for tnt being FinSequence holds not y ==> tnt ) ) by Lm6;
( y = O or ( y = S & {O,S} <> {} ) ) by Lm2, TARSKI:def 2;
hence x in {O} by A1, Lm4, TARSKI:def 1; :: thesis: verum