theorem Th14: :: TREES_2:14

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