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 b1 being FinSequence of omega holds
( not b1 in T or ProperPrefixes b1 c= T ) ) & ( for b1 being FinSequence of omega
for b2, b3 being set holds
( not b1 ^ <*b2*> in T or not b3 <= b2 or b1 ^ <*b3*> in T ) ) )
thus for p being FinSequence of NAT st p in T holds
ProperPrefixes p c= T :: thesis: for b1 being FinSequence of omega
for b2, b3 being set holds
( not b1 ^ <*b2*> in T or not b3 <= b2 or b1 ^ <*b3*> 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 b1, b2 being set holds
( not p ^ <*b1*> in T or not b2 <= b1 or p ^ <*b2*> 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