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;
A2: x c= union D by ZFMISC_1:92;
reconsider T = union D as non empty set by A2;
A3: T is Tree-like

proof

A4: 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 A5: X in D ; :: thesis: X c= NAT *
A6: X is Tree by A1, A5;
thus X c= NAT * by A6, TREES_1:def 5; :: thesis: verum

end;

thus T c= NAT * by A4, 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 A7: p in T ; :: thesis: ProperPrefixes p c= T
consider X being set such that
A8: p in X and
A9: X in D by A7, TARSKI:def 4;
reconsider X = X as Tree by A1, A9;
A10: ( ProperPrefixes p c= X & X c= T ) by A8, A9, TREES_1:def 5, ZFMISC_1:92;
thus ProperPrefixes p c= T by A10, 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 that
A11: p ^ <*k*> in T and
A12: n <= k ; :: thesis: p ^ <*n*> in T
consider X being set such that
A13: p ^ <*k*> in X and
A14: X in D by A11, TARSKI:def 4;
reconsider X = X as Tree by A1, A14;
A15: p ^ <*n*> in X by A12, A13, TREES_1:def 5;
thus p ^ <*n*> in T by A14, A15, TARSKI:def 4; :: thesis: verum

end;

thus union D is Tree by A3; :: thesis: verum