let p be FinSequence of NAT ; :: according to TREES_2:def 1 :: thesis: ( ( not p in tree {} or p in elementary_tree 0 ) & ( not p in elementary_tree 0 or p in tree {} ) )
thus ( p in tree {} implies p in elementary_tree 0 ) :: thesis: ( not p in elementary_tree 0 or p in tree {} )

proof

assume p in tree {} ; :: thesis: p in elementary_tree 0
then A1: ( p = {} or ex n being Nat ex q being FinSequence st
( n < len {} & q in {} . (n + 1) & p = <*n*> ^ q ) ) by Def15;
assume not p in elementary_tree 0 ; :: thesis: contradiction
hence contradiction by A1, TARSKI:def 1, TREES_1:29; :: thesis: verum

end;

assume p in elementary_tree 0 ; :: thesis: p in tree {}
then p = {} by TARSKI:def 1, TREES_1:29;
hence p in tree {} by Def15; :: thesis: verum