set D = T /\ T1;
thus
T /\ T1 is Tree-like
not T /\ T1 is empty proof
(
T c= NAT * &
T /\ T1 c= T )
by Def3, XBOOLE_1:17;
hence
T /\ T1 c= NAT *
;
TREES_1:def 3 ( ( 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
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
let p be
FinSequence of
NAT ;
for k, n being Nat st p ^ <*k*> in T /\ T1 & n <= k holds
p ^ <*n*> in T /\ T1let k,
n be
Nat;
( p ^ <*k*> in T /\ T1 & n <= k implies p ^ <*n*> in T /\ T1 )
assume that A8:
p ^ <*k*> in T /\ T1
and A9:
n <= k
;
p ^ <*n*> in T /\ T1
A10:
p ^ <*k*> in T
by A8, XBOOLE_0:def 4;
A11:
p ^ <*k*> in T1
by A8, XBOOLE_0:def 4;
A12:
p ^ <*n*> in T
by A9, A10, Def3;
p ^ <*n*> in T1
by A9, A11, Def3;
hence
p ^ <*n*> in T /\ T1
by A12, XBOOLE_0:def 4;
verum
end;
( {} in T & {} in T1 )
by Th21;
hence
not T /\ T1 is empty
by XBOOLE_0:def 4; verum