set D = T \/ T1;
( T c= NAT * & T1 c= NAT * ) by Def3;
hence T \/ T1 c= NAT * by XBOOLE_1:8; :: according to TREES_1:def 3 :: thesis: ( ( for p being FinSequence of NAT st p in T \/ T1 holds
ProperPrefixes p c= T \/ T1 ) & ( for p being FinSequence of NAT
for k, n being Nat st p ^ <*k*> in T \/ T1 & n <= k holds
p ^ <*n*> in T \/ T1 ) )
thus for p being FinSequence of NAT st p in T \/ T1 holds
ProperPrefixes p c= T \/ T1 :: thesis: for p being FinSequence of NAT
for k, n being Nat st p ^ <*k*> in T \/ T1 & n <= k holds
p ^ <*n*> in T \/ T1

proof

let p be FinSequence of NAT ; :: thesis: ( p in T \/ T1 implies ProperPrefixes p c= T \/ T1 )
assume p in T \/ T1 ; :: thesis: ProperPrefixes p c= T \/ T1
then ( p in T or p in T1 ) by XBOOLE_0:def 3;
then A1: ( ProperPrefixes p c= T or ProperPrefixes p c= T1 ) by Def3;
( T c= T \/ T1 & T1 c= T \/ T1 ) by XBOOLE_1:7;
hence ProperPrefixes p c= T \/ T1 by A1; :: thesis: verum

end;

let p be FinSequence of NAT ; :: thesis: for k, n being Nat st p ^ <*k*> in T \/ T1 & n <= k holds
p ^ <*n*> in T \/ T1
let k, n be Nat; :: thesis: ( p ^ <*k*> in T \/ T1 & n <= k implies p ^ <*n*> in T \/ T1 )
assume that
A2: p ^ <*k*> in T \/ T1 and
A3: n <= k ; :: thesis: p ^ <*n*> in T \/ T1
( p ^ <*k*> in T or p ^ <*k*> in T1 ) by A2, XBOOLE_0:def 3;
then ( p ^ <*n*> in T or p ^ <*n*> in T1 ) by A3, Def3;
hence p ^ <*n*> in T \/ T1 by XBOOLE_0:def 3; :: thesis: verum