assume not (-) X is empty ; :: thesis: contradiction
then consider x being set such that
A1: x in (-) X by XBOOLE_0:def 1;
reconsider x = x as Element of (-) X by A1;
- (- x) = x ;
hence contradiction by A1, Def3; :: thesis: verum