A1: now

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

proof

assume A2: x in {{} ,<*0 *>} ; :: thesis: ( x in { <*n*> where n is Element of NAT : n < 1 } or x in {{} } )
A3: ( x = {} or x = <*0 *> ) by A2, TARSKI:def 2;
thus ( x in { <*n*> where n is Element of NAT : n < 1 } or x in {{} } ) by A3, TARSKI:def 1; :: thesis: verum

end;

assume A4: ( x in { <*n*> where n is Element of NAT : n < 1 } or x in {{} } ) ; :: thesis: x in {{} ,<*0 *>}

A5: now

per cases ( x in { <*n*> where n is Element of NAT : n < 1 } or x in {{} } ) by A4;

suppose A6: x in { <*n*> where n is Element of NAT : n < 1 } ; :: thesis: x in {{} ,<*0 *>}

consider n being Element of NAT such that
A7: x = <*n*> and
A8: n < 1 by A6;
A9: n = 0 by A8, NAT_1:26;
thus x in {{} ,<*0 *>} by A7, A9, TARSKI:def 2; :: thesis: verum

end;

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

A11: x = {} by A10, TARSKI:def 1;
thus x in {{} ,<*0 *>} by A11, TARSKI:def 2; :: thesis: verum

end;

end;

end;

thus x in {{} ,<*0 *>} by A5; :: thesis: verum

end;

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