let X be Tolerance_Space; :: thesis: for A being RoughSet of X ex B, C being Subset of X st A = [B,C]
let A be RoughSet of X; :: thesis: ex B, C being Subset of X st A = [B,C]
consider A1, A2 being object such that
A1: ( A1 in bool the carrier of X & A2 in bool the carrier of X & A = [A1,A2] ) by ZFMISC_1:def 2;
reconsider A1 = A1, A2 = A2 as Subset of X by A1;
take A1 ; :: thesis: ex C being Subset of X st A = [A1,C]
take A2 ; :: thesis: A = [A1,A2]
thus A = [A1,A2] by A1; :: thesis: verum