for W being finite Tree holds W = union { (W -level n) where n is Nat : n <= height W }