let i, n be Real; :: thesis: ( not |.i.| = n or i = n or i = - n )
assume ( |.i.| = n & i <> n ) ; :: thesis: i = - n
then n = - i by ABSVALUE:def 1;
hence i = - n ; :: thesis: verum