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

proof

A3: ( T c= NAT * & T /\ T1 c= T ) by Def5, XBOOLE_1:17;
thus D c= NAT * by A3, 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
A5: p in T by A4, XBOOLE_0:def 4;
A6: p in T1 by A4, XBOOLE_0:def 4;
A7: ProperPrefixes p c= T by A5, Def5;
A8: ProperPrefixes p c= T1 by A6, Def5;
thus ProperPrefixes p c= D by A7, A8, 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;
A14: p ^ <*n*> in T1 by A10, A12, Def5;
thus p ^ <*n*> in D by A13, A14, XBOOLE_0:def 4; :: thesis: verum

end;

thus T /\ T1 is Tree by A2; :: thesis: verum