let i, j be Nat; :: thesis: ( elementary_tree i = elementary_tree j implies i = j )
assume elementary_tree i = elementary_tree j ; :: thesis: i = j
then ( i <= j & i >= j ) by Th1;
hence i = j by XXREAL_0:1; :: thesis: verum