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

proof

let x be object ; :: 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:22;
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 object ; :: 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; :: thesis: verum