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