let T be Tree; :: thesis: T -level 0 = {{} }
{ w where w is Element of T : len w = 0 } = {{} }

proof

thus { w where w is Element of T : len w = 0 } c= {{} } :: according to XBOOLE_0:def 10 :: thesis: {{} } c= { w where w is Element of T : len w = 0 }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { w where w is Element of T : len w = 0 } or x in {{} } )
assume x in { w where w is Element of T : len w = 0 } ; :: thesis: x in {{} }
then consider w being Element of T such that
A1: ( w = x & len w = 0 ) ;
w = {} by A1;
hence x in {{} } by A1, TARSKI:def 1; :: thesis: verum

end;

thus {{} } c= { w where w is Element of T : len w = 0 } :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {{} } or x in { w where w is Element of T : len w = 0 } )
assume x in {{} } ; :: thesis: x in { w where w is Element of T : len w = 0 }
then A2: x = {} by TARSKI:def 1;
{} in T by TREES_1:47;
then consider t being Element of T such that
A3: t = {} ;
len t = 0 by A3;
hence x in { w where w is Element of T : len w = 0 } by A2, A3; :: thesis: verum

end;

end;

hence T -level 0 = {{} } ; :: thesis: verum