let n be 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 object ; :: 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 ;
t | (Seg n) is FinSequence of NAT by FINSEQ_1:18;
then consider s being FinSequence of NAT such that
A2: s = t | (Seg n) ;
s is_a_prefix_of t by A2, TREES_1:def 1;
then reconsider s = s as Element of T by TREES_1:20;
A3: ex w9 being Element of T st
( t = w9 & len w9 = n + 1 ) by A1;
n + 0 <= n + 1 by XREAL_1:6;
then len s = n by A3, A2, FINSEQ_1:17;
then A4: succ s in { (succ w) where w is Element of T : len w = n } ;
Seg (n + 1) = dom t by A3, FINSEQ_1:def 3;
then t = t | (Seg (n + 1)) ;
then ex m being Element of NAT st t = s ^ <*m*> by A3, A2, Th33;
then t in succ s ;
hence x in union { (succ w) where w is Element of T : len w = n } by A4, 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

set X = { (succ w) where w is Element of T : len w = n } ;
let x be object ; :: 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) )
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
A5: x in Y and
A6: 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
A7: Y = succ w and
A8: len w = n by A6;
reconsider t = x as Element of T by A5, A7;
consider k being Nat such that
A9: t = w ^ <*k*> and
w ^ <*k*> in T by A5, A7;
len <*k*> = 1 by FINSEQ_1:40;
then len t = n + 1 by A8, A9, FINSEQ_1:22;
hence x in T -level (n + 1) ; :: thesis: verum

end;