let T be Tree; :: thesis: T -level 0 = {{} }
A1: {{} } 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 {{} } 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;

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

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
A4: w = x and
A5: len w = 0 ;
w = {} by A5;
hence x in {{} } by A4, TARSKI:def 1; :: thesis: verum

end;

hence T -level 0 = {{} } by A1, XBOOLE_0:def 10; :: thesis: verum