thus {{}} c= NAT * :: according to TREES_1:def 3 :: thesis: ( ( for p being FinSequence of NAT st p in {{}} holds
ProperPrefixes p c= {{}} ) & ( for p being FinSequence of NAT
for k, n being Nat st p ^ <*k*> in {{}} & n <= k holds
p ^ <*n*> in {{}} ) )

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {{}} or x in NAT * )
assume x in {{}} ; :: thesis: x in NAT *
then x = {} by TARSKI:def 1;
hence x in NAT * by FINSEQ_1:49; :: thesis: verum

end;

thus for p being FinSequence of NAT st p in {{}} holds
ProperPrefixes p c= {{}} by TARSKI:def 1, Th14; :: thesis: for p being FinSequence of NAT
for k, n being Nat st p ^ <*k*> in {{}} & n <= k holds
p ^ <*n*> in {{}}
thus for p being FinSequence of NAT
for k, n being Nat st p ^ <*k*> in {{}} & n <= k holds
p ^ <*n*> in {{}} by TARSKI:def 1; :: thesis: verum