theorem :: TREES_1:26

for fT, fT1 being finite Tree holds fT \/ fT1 is finite Tree ;