reconsider A = {} as Subset of X by XBOOLE_1:2;
A = {} X ;
then A1: ( LAp A = {} & UAp A = {} ) by ROUGHS_1:18, ROUGHS_1:19;
[(LAp A),(UAp A)] in [:(bool the carrier of X),(bool the carrier of X):] by ZFMISC_1:87;
hence [{},{}] is RoughSet of X by Def13, A1; :: thesis: verum