let n be Element of NAT ; :: thesis: for T being Tree holds T -level (n + 1) = union { (succ w) where w is Element of T : len w = n }
let T be Tree; :: thesis: T -level (n + 1) = union { (succ w) where w is Element of T : len w = n }
thus T -level (n + 1) c= union { (succ w) where w is Element of T : len w = n } :: according to XBOOLE_0:def 10 :: thesis: union { (succ w) where w is Element of T : len w = n } c= T -level (n + 1)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in T -level (n + 1) or x in union { (succ w) where w is Element of T : len w = n } )
assume A1: x in T -level (n + 1) ; :: thesis: x in union { (succ w) where w is Element of T : len w = n }
then reconsider t = x as Element of T ;
consider w' being Element of T such that
A2: ( t = w' & len w' = n + 1 ) by A1;
t | (Seg n) is FinSequence of NAT by FINSEQ_1:23;
then consider s being FinSequence of NAT such that
A3: s = t | (Seg n) ;
s is_a_prefix_of t by A3, TREES_1:def 1;
then reconsider s = s as Element of T by TREES_1:45;
n + 0 <= n + 1 by XREAL_1:8;
then A4: len s = n by A2, A3, FINSEQ_1:21;
Seg (n + 1) = dom t by A2, FINSEQ_1:def 3;
then ( n + 1 <= len t & t = t | (Seg (n + 1)) ) by A2, RELAT_1:98;
then consider m being Element of NAT such that
A5: t = s ^ <*m*> by A3, Th6;
A6: t in succ s by A5;
succ s in { (succ w) where w is Element of T : len w = n } by A4;
hence x in union { (succ w) where w is Element of T : len w = n } by A6, TARSKI:def 4; :: thesis: verum

end;

thus union { (succ w) where w is Element of T : len w = n } c= T -level (n + 1) :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union { (succ w) where w is Element of T : len w = n } or x in T -level (n + 1) )
set X = { (succ w) where w is Element of T : len w = n } ;
assume x in union { (succ w) where w is Element of T : len w = n } ; :: thesis: x in T -level (n + 1)
then consider Y being set such that
A7: ( x in Y & Y in { (succ w) where w is Element of T : len w = n } ) by TARSKI:def 4;
consider w being Element of T such that
A8: ( Y = succ w & len w = n ) by A7;
reconsider t = x as Element of T by A7, A8;
consider k being Element of NAT such that
A9: ( t = w ^ <*k*> & w ^ <*k*> in T ) by A7, A8;
len <*k*> = 1 by FINSEQ_1:57;
then len t = n + 1 by A8, A9, FINSEQ_1:35;
hence x in T -level (n + 1) ; :: thesis: verum

end;