A1: now

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

end;

thus elementary_tree 0 = {{} } by A1; :: thesis: verum