let W be Tree; :: thesis: for L being Level of W ex n being Element of NAT st L = W -level n
let L be Level of W; :: thesis: ex n being Element of 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 Element of NAT by ORDINAL1:def 13;
take n ; :: thesis: L = W -level n
thus L = W -level n by A1; :: thesis: verum