now

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

end;

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