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

proof

A2: ( T c= NAT * & T1 c= NAT * ) by Def5;
thus D c= NAT * by A2, 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 A3: p in D ; :: thesis: ProperPrefixes p c= D
A4: ( p in T or p in T1 ) by A3, XBOOLE_0:def 3;
A5: ( ProperPrefixes p c= T or ProperPrefixes p c= T1 ) by A4, Def5;
A6: ( T c= D & T1 c= D ) by XBOOLE_1:7;
thus ProperPrefixes p c= D by A5, A6, 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
A9: ( p ^ <*k*> in T or p ^ <*k*> in T1 ) by A7, XBOOLE_0:def 3;
A10: ( p ^ <*n*> in T or p ^ <*n*> in T1 ) by A8, A9, Def5;
thus p ^ <*n*> in D by A10, XBOOLE_0:def 3; :: thesis: verum

end;

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