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