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