let D be non empty set ; :: thesis: ( ( for x being set st x in D holds
x is Tree ) implies union D is Tree )
assume A1: for x being set st x in D holds
x is Tree ; :: thesis: union D is Tree
consider x being Element of D;
reconsider x = x as Tree by A1;
consider y being Element of x;
( y in x & x c= union D ) by ZFMISC_1:92;
then reconsider T = union D as non empty set ;
T is Tree-like

proof

for X being set st X in D holds
X c= NAT *

proof

let X be set ; :: thesis: ( X in D implies X c= NAT * )
assume X in D ; :: thesis: X c= NAT *
then X is Tree by A1;
hence X c= NAT * by TREES_1:def 5; :: thesis: verum

end;

hence T c= NAT * by ZFMISC_1:94; :: according to TREES_1:def 5 :: thesis: ( ( for b₁ being FinSequence of NAT holds
( not b₁ in T or ProperPrefixes b₁ c= T ) ) & ( for b₁ being FinSequence of NAT
for b₂, b₃ being Element of NAT holds
( not b₁ ^ <*b₂*> in T or not b₃ <= b₂ or b₁ ^ <*b₃*> in T ) ) )
thus for p being FinSequence of NAT st p in T holds
ProperPrefixes p c= T :: thesis: for b₁ being FinSequence of NAT
for b₂, b₃ being Element of NAT holds
( not b₁ ^ <*b₂*> in T or not b₃ <= b₂ or b₁ ^ <*b₃*> in T )

proof

let p be FinSequence of NAT ; :: thesis: ( p in T implies ProperPrefixes p c= T )
assume p in T ; :: thesis: ProperPrefixes p c= T
then consider X being set such that
A2: ( p in X & X in D ) by TARSKI:def 4;
reconsider X = X as Tree by A1, A2;
( ProperPrefixes p c= X & X c= T ) by A2, TREES_1:def 5, ZFMISC_1:92;
hence ProperPrefixes p c= T by XBOOLE_1:1; :: thesis: verum

end;

let p be FinSequence of NAT ; :: thesis: for b₁, b₂ being Element of NAT holds
( not p ^ <*b₁*> in T or not b₂ <= b₁ or p ^ <*b₂*> in T )
let k, n be Element of NAT ; :: thesis: ( not p ^ <*k*> in T or not n <= k or p ^ <*n*> in T )
assume A3: ( p ^ <*k*> in T & n <= k ) ; :: thesis: p ^ <*n*> in T
then consider X being set such that
A4: ( p ^ <*k*> in X & X in D ) by TARSKI:def 4;
reconsider X = X as Tree by A1, A4;
p ^ <*n*> in X by A3, A4, TREES_1:def 5;
hence p ^ <*n*> in T by A4, TARSKI:def 4; :: thesis: verum

end;

hence union D is Tree ; :: thesis: verum