let x be object ; :: 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 and
A2: for tnt being FinSequence holds not y ==> tnt by Lm7;
( y = O or ( y = S & {O,S} <> {} ) ) by Lm2, TARSKI:def 2;
hence x in {O} by A1, A2, Lm5, TARSKI:def 1; :: thesis: verum