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