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 p in D ; :: thesis: ProperPrefixes p c= D
then ( p in T & p in T1 ) by XBOOLE_0:def 4;
then ( ProperPrefixes p c= T & ProperPrefixes p c= T1 ) by Def5;
hence ProperPrefixes p c= D by 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 A1: ( p ^ <*k*> in D & n <= k ) ; :: thesis: p ^ <*n*> in D
then ( p ^ <*k*> in T & p ^ <*k*> in T1 ) by XBOOLE_0:def 4;
then ( p ^ <*n*> in T & p ^ <*n*> in T1 ) by A1, Def5;
hence p ^ <*n*> in D by XBOOLE_0:def 4; :: thesis: verum

end;

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