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