{} in W by TREES_1:22;
then reconsider L = {{}} as Subset of W by ZFMISC_1:31;
take L ; :: thesis: ex n being Nat st L = { w where w is Element of W : len w = n }
take 0 ; :: thesis: L = { w where w is Element of W : len w = 0 }
thus L c= { w where w is Element of W : len w = 0 } :: according to XBOOLE_0:def 10 :: thesis: { w where w is Element of W : len w = 0 } c= L

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in L or x in { w where w is Element of W : len w = 0 } )
assume A1: x in L ; :: thesis: x in { w where w is Element of W : len w = 0 }
then A2: x = {} by TARSKI:def 1;
len {} = 0 ;
hence x in { w where w is Element of W : len w = 0 } by A1, A2; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { w where w is Element of W : len w = 0 } or x in L )
assume x in { w where w is Element of W : len w = 0 } ; :: thesis: x in L
then ex w being Element of W st
( x = w & len w = 0 ) ;
then x = {} ;
hence x in L by TARSKI:def 1; :: thesis: verum