theorem :: TREES_1:25

for T, T1 being Tree holds T /\ T1 is Tree ;