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

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