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 A2: x in W -level 1 ; :: thesis: x in succ w
consider w9 being Element of W such that
A3: x = w9 and
A4: len w9 = 1 by A2;
A5: w9 = <*(w9 . 1)*> by A4, FINSEQ_1:57;
A6: rng w9 = {(w9 . 1)} by A5, FINSEQ_1:56;
reconsider n = w9 . 1 as Element of NAT by A6, ZFMISC_1:37;
A7: w9 = w ^ <*n*> by A1, A5, FINSEQ_1:47;
thus x in succ w by A3, A7; :: 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 A8: x in succ w ; :: thesis: x in W -level 1
consider i being Element of NAT such that
A9: x = w ^ <*i*> and
A10: w ^ <*i*> in W by A8;
reconsider w9 = w ^ <*i*> as Element of W by A10;
A11: ( len <*i*> = 1 & w9 = <*i*> ) by A1, FINSEQ_1:47, FINSEQ_1:56;
thus x in W -level 1 by A9, A11; :: thesis: verum