[((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