[(LAp A),(UAp A)] in [:(bool the carrier of X),(bool the carrier of X):] by ZFMISC_1:87;
hence [(LAp A),(UAp A)] is RoughSet of X by Def13; :: thesis: verum