consider A being RoughSet of X;
A in RoughSets X by DefRSX;
hence not RoughSets X is empty ; :: thesis: verum