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 Def5, XBOOLE_1:17;
hence T /\ T1 c= NAT * by XBOOLE_1:1; :: 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 Element of 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 Element of 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 A1: p in T /\ T1 ; :: thesis: ProperPrefixes p c= T /\ T1
then A2: p in T by XBOOLE_0:def 4;
A3: p in T1 by A1, XBOOLE_0:def 4;
A4: ProperPrefixes p c= T by A2, Def5;
ProperPrefixes p c= T1 by A3, Def5;
hence ProperPrefixes p c= T /\ T1 by A4, XBOOLE_1:19; :: thesis: verum

end;

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

end;

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