now

consider x being Element of { <*j*> where j is Element of NAT : j < 0 } ;
assume { <*j*> where j is Element of NAT : j < 0 } <> {} ; :: thesis: contradiction
then x in { <*j*> where j is Element of NAT : j < 0 } ;
then ex k being Element of NAT st
( x = <*k*> & k < 0 ) ;
hence contradiction ; :: thesis: verum

end;

hence elementary_tree 0 = {{} } ; :: thesis: verum