theorem :: TREES_1:27

for T being Tree
for fT being finite Tree holds fT /\ T is finite Tree ;