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

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