let X be Tolerance_Space; for A being RoughSet of X ex B, C being Subset of X st A = [B,C]
let A be RoughSet of X; 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
; ex C being Subset of X st A = [A1,C]
take
A2
; A = [A1,A2]
thus
A = [A1,A2]
by A1; verum