for x being object holds
( x in Leaves (elementary_tree 0) iff x in elementary_tree 0 )

proof

let x be object ; :: thesis: ( x in Leaves (elementary_tree 0) iff x in elementary_tree 0 )
thus ( x in Leaves (elementary_tree 0) implies x in elementary_tree 0 ) ; :: thesis: ( x in elementary_tree 0 implies x in Leaves (elementary_tree 0) )
assume x in elementary_tree 0 ; :: thesis: x in Leaves (elementary_tree 0)
then reconsider x0 = x as Element of elementary_tree 0 ;
not x0 ^ <*0*> in elementary_tree 0 by TREES_1:29, TARSKI:def 1;
hence x in Leaves (elementary_tree 0) by TREES_1:54; :: thesis: verum

end;

hence Leaves (elementary_tree 0) = elementary_tree 0 by TARSKI:2; :: thesis: verum