reconsider A = [#] X as Subset of X ;
A1: ( LAp A = [#] X & UAp A = [#] X ) by ROUGHS_1:20, ROUGHS_1:21;
[(LAp A),(UAp A)] in [:(bool the carrier of X),(bool the carrier of X):] by ZFMISC_1:87;
hence [([#] X),([#] X)] is RoughSet of X by Def13, A1; :: thesis: verum