the carrier of (RSLattice X) = RoughSets X by Def8;
hence not RSLattice X is empty ; :: thesis: verum