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
then reconsider x = the Element of D as Tree ;
x c= union D by ZFMISC_1:74;
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 3; :: thesis: verum

end;

hence T c= NAT * by ZFMISC_1:76; :: according to TREES_1:def 3 :: thesis: ( ( for b₁ being FinSequence of omega holds
( not b₁ in T or ProperPrefixes b₁ c= T ) ) & ( for b₁ being FinSequence of omega
for b₂, b₃ being set 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 omega
for b₂, b₃ being set 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 and
A3: X in D by TARSKI:def 4;
reconsider X = X as Tree by A1, A3;
( ProperPrefixes p c= X & X c= T ) by A2, A3, TREES_1:def 3, ZFMISC_1:74;
hence ProperPrefixes p c= T ; :: thesis: verum

end;

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

end;

hence union D is Tree ; :: thesis: verum