let W be Tree; :: thesis: for L being Level of W ex n being Nat st L = W -level n
let L be Level of W; :: thesis: ex n being Nat st L = W -level n
consider n being Nat such that
A1: L = { w where w is Element of W : len w = n } by Def4;
reconsider n = n as Nat ;
take n ; :: thesis: L = W -level n
thus L = W -level n by A1; :: thesis: verum