consider x being Element of X;
- x = - x ;
hence not - X is empty by Def6; :: thesis: verum