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 object ; :: 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
A2: x = w9 and
A3: len w9 = 1 ;
A4: w9 = <*(w9 . 1)*> by A3, FINSEQ_1:40;
then rng w9 = {(w9 . 1)} by FINSEQ_1:39;
then reconsider n = w9 . 1 as Element of NAT by ZFMISC_1:31;
w9 = w ^ <*n*> by A1, A4, FINSEQ_1:34;
hence x in succ w by A2; :: thesis: verum

end;

let x be object ; :: 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 Nat such that
A5: x = w ^ <*i*> and
A6: w ^ <*i*> in W ;
reconsider w9 = w ^ <*i*> as Element of W by A6;
( len <*i*> = 1 & w9 = <*i*> ) by A1, FINSEQ_1:34, FINSEQ_1:39;
hence x in W -level 1 by A5; :: thesis: verum