now

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

proof

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

end;

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

now

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

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

then consider n being Element of NAT such that
A7: x = <*n*> and
A8: n < 2 ;
( n = 0 or n = 1 ) by A8, NAT_1:27;
hence x in {{} ,<*0 *>,<*1*>} by A7, ENUMSET1:def 1; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

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