let x be object ; :: according to VALUED_2:def 4 :: thesis: ( not x in (-) X or x is set )
assume A1: x in (-) X ; :: thesis: x is set
then reconsider x = x as Element of (-) X ;
A2: - x in X by A1, Th24;
( - (- x) = x & (-) ((-) X) = X ) ;
hence x is set by A2; :: thesis: verum