set D = T /\ T1;
thus T /\ T1 is Tree-like :: thesis: not T /\ T1 is empty

proof

( T c= NAT * & T /\ T1 c= T ) by Def3, XBOOLE_1:17;
hence T /\ T1 c= NAT * ; :: according to TREES_1:def 3 :: thesis: ( ( for p being FinSequence of NAT st p in T /\ T1 holds
ProperPrefixes p c= T /\ T1 ) & ( for p being FinSequence of NAT
for k, n being Nat st p ^ <*k*> in T /\ T1 & n <= k holds
p ^ <*n*> in T /\ T1 ) )
thus for p being FinSequence of NAT st p in T /\ T1 holds
ProperPrefixes p c= T /\ T1 :: thesis: for p being FinSequence of NAT
for k, n being Nat st p ^ <*k*> in T /\ T1 & n <= k holds
p ^ <*n*> in T /\ T1

proof

let p be FinSequence of NAT ; :: thesis: ( p in T /\ T1 implies ProperPrefixes p c= T /\ T1 )
assume A4: p in T /\ T1 ; :: thesis: ProperPrefixes p c= T /\ T1
then A5: p in T by XBOOLE_0:def 4;
A6: p in T1 by A4, XBOOLE_0:def 4;
A7: ProperPrefixes p c= T by A5, Def3;
ProperPrefixes p c= T1 by A6, Def3;
hence ProperPrefixes p c= T /\ T1 by A7, XBOOLE_1:19; :: thesis: verum

end;

let p be FinSequence of NAT ; :: thesis: for k, n being Nat st p ^ <*k*> in T /\ T1 & n <= k holds
p ^ <*n*> in T /\ T1
let k, n be Nat; :: thesis: ( p ^ <*k*> in T /\ T1 & n <= k implies p ^ <*n*> in T /\ T1 )
assume that
A8: p ^ <*k*> in T /\ T1 and
A9: n <= k ; :: thesis: p ^ <*n*> in T /\ T1
A10: p ^ <*k*> in T by A8, XBOOLE_0:def 4;
A11: p ^ <*k*> in T1 by A8, XBOOLE_0:def 4;
A12: p ^ <*n*> in T by A9, A10, Def3;
p ^ <*n*> in T1 by A9, A11, Def3;
hence p ^ <*n*> in T /\ T1 by A12, XBOOLE_0:def 4; :: thesis: verum

end;

( {} in T & {} in T1 ) by Th21;
hence not T /\ T1 is empty by XBOOLE_0:def 4; :: thesis: verum