let W be Tree; :: thesis: for w being Element of W st w = {} holds
W -level 1 = succ w
let w be Element of W; :: thesis: ( w = {} implies W -level 1 = succ w )
assume A1: w = {} ; :: thesis: W -level 1 = succ w
thus W -level 1 c= succ w :: according to XBOOLE_0:def 10 :: thesis: succ w c= W -level 1

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in W -level 1 or x in succ w )
assume x in W -level 1 ; :: thesis: x in succ w
then consider w9 being Element of W such that
A3: x = w9 and
A4: len w9 = 1 ;
A5: w9 = <*(w9 . 1)*> by A4, FINSEQ_1:57;
then rng w9 = {(w9 . 1)} by FINSEQ_1:56;
then reconsider n = w9 . 1 as Element of NAT by ZFMISC_1:37;
w9 = w ^ <*n*> by A1, A5, FINSEQ_1:47;
hence x in succ w by A3; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in succ w or x in W -level 1 )
assume x in succ w ; :: thesis: x in W -level 1
then consider i being Element of NAT such that
A9: x = w ^ <*i*> and
A10: w ^ <*i*> in W ;
reconsider w9 = w ^ <*i*> as Element of W by A10;
( len <*i*> = 1 & w9 = <*i*> ) by A1, FINSEQ_1:47, FINSEQ_1:56;
hence x in W -level 1 by A9; :: thesis: verum