let T, T1 be Tree; :: thesis: T \/ T1 is Tree
reconsider D = T \/ T1 as non empty set ;
D is Tree-like

proof

( T c= NAT * & T1 c= NAT * ) by Def5;
hence D c= NAT * by XBOOLE_1:8; :: 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 or p in T1 ) by XBOOLE_0:def 3;
then A5: ( ProperPrefixes p c= T or ProperPrefixes p c= T1 ) by Def5;
( T c= D & T1 c= D ) by XBOOLE_1:7;
hence ProperPrefixes p c= D by A5, XBOOLE_1:1; :: 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
A7: p ^ <*k*> in D and
A8: n <= k ; :: thesis: p ^ <*n*> in D
( p ^ <*k*> in T or p ^ <*k*> in T1 ) by A7, XBOOLE_0:def 3;
then ( p ^ <*n*> in T or p ^ <*n*> in T1 ) by A8, Def5;
hence p ^ <*n*> in D by XBOOLE_0:def 3; :: thesis: verum

end;

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