now :: thesis: not { <*j*> where j is Nat : j < 0 } <> {}

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

end;

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