now :: thesis: for x being object holds
( ( not x in {{},<*0*>} or x in { <*n*> where n is Nat : n < 1 } or x in {{}} ) & ( ( x in { <*n*> where n is Nat : n < 1 } or x in {{}} ) implies x in {{},<*0*>} ) )

let x be object ; :: thesis: ( ( not x in {{},<*0*>} or x in { <*n*> where n is Nat : n < 1 } or x in {{}} ) & ( ( x in { <*n*> where n is Nat : n < 1 } or x in {{}} ) implies x in {{},<*0*>} ) )
thus ( not x in {{},<*0*>} or x in { <*n*> where n is Nat : n < 1 } or x in {{}} ) :: thesis: ( ( x in { <*n*> where n is Nat : n < 1 } or x in {{}} ) implies x in {{},<*0*>} )

proof

assume x in {{},<*0*>} ; :: thesis: ( x in { <*n*> where n is Nat : n < 1 } or x in {{}} )
then ( x = {} or x = <*0*> ) by TARSKI:def 2;
hence ( x in { <*n*> where n is Nat : n < 1 } or x in {{}} ) by TARSKI:def 1; :: thesis: verum

end;

assume A1: ( x in { <*n*> where n is Nat : n < 1 } or x in {{}} ) ; :: thesis: x in {{},<*0*>}

now :: thesis: x in {{},<*0*>}

per cases ( x in { <*n*> where n is Nat : n < 1 } or x in {{}} ) by A1;

suppose x in { <*n*> where n is Nat : n < 1 } ; :: thesis: x in {{},<*0*>}

then consider n being Nat such that
A2: x = <*n*> and
A3: n < 1 ;
n = 0 by A3, NAT_1:25;
hence x in {{},<*0*>} by A2, TARSKI:def 2; :: thesis: verum

end;

suppose x in {{}} ; :: thesis: x in {{},<*0*>}

then x = {} by TARSKI:def 1;
hence x in {{},<*0*>} by TARSKI:def 2; :: thesis: verum

end;

end;

end;

hence x in {{},<*0*>} ; :: thesis: verum

end;

hence elementary_tree 1 = {{},<*0*>} by XBOOLE_0:def 3; :: thesis: verum