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 w' being Element of W such that
A2: ( x = w' & len w' = 1 ) ;
A3: w' = <*(w' . 1)*> by A2, FINSEQ_1:57;
then ( rng w' c= NAT & rng w' = {(w' . 1)} ) by FINSEQ_1:56;
then reconsider n = w' . 1 as Element of NAT by ZFMISC_1:37;
( w' = w ^ <*n*> & w' in W ) by A1, A3, FINSEQ_1:47;
hence x in succ w by A2; :: 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
A4: ( x = w ^ <*i*> & w ^ <*i*> in W ) ;
reconsider w' = w ^ <*i*> as Element of W by A4;
( len <*i*> = 1 & w' = <*i*> ) by A1, FINSEQ_1:47, FINSEQ_1:56;
hence x in W -level 1 by A4; :: thesis: verum