A1: {} in W by TREES_1:47;
reconsider L = {{} } as Subset of W by A1, ZFMISC_1:37;
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 set ; :: according to TARSKI:def 3 :: thesis: ( not x in L or x in { w where w is Element of W : len w = 0 } )
assume A2: x in L ; :: thesis: x in { w where w is Element of W : len w = 0 }
A3: x = {} by A2, TARSKI:def 1;
A4: len {} = 0 ;
thus x in { w where w is Element of W : len w = 0 } by A2, A3, A4; :: thesis: verum

end;

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