let i, j be Element of NAT ; :: thesis: ( elementary_tree i = elementary_tree j implies i = j )
assume A1: elementary_tree i = elementary_tree j ; :: thesis: i = j
A2: ( i <= j & i >= j ) by A1, Th1;
thus i = j by A2, XXREAL_0:1; :: thesis: verum