set A = the RoughSet of X;
the RoughSet of X in RoughSets X by Def20;
hence not RoughSets X is empty ; :: thesis: verum