let T, T1 be Tree; :: thesis: T /\ T1 is Tree
( {} in T & {} in T1 ) by Th47;
then reconsider D = T /\ T1 as non empty set by XBOOLE_0:def 4;
D is Tree-like

proof

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

proof

let p be FinSequence of NAT ; :: thesis: ( p in D implies ProperPrefixes p c= D )
assume A4: p in D ; :: thesis: ProperPrefixes p c= D
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, Def5;
ProperPrefixes p c= T1 by A6, Def5;
hence ProperPrefixes p c= D by A7, XBOOLE_1:19; :: thesis: verum

end;

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

end;

hence T /\ T1 is Tree ; :: thesis: verum