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