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