let X be Tolerance_Space; :: thesis: for A, B being Element of
for A', B' being RoughSet of X st A = A' & B = B' holds
( A [= B iff ( LAp A' c= LAp B' & UAp A' c= UAp B' ) )
let A, B be Element of ; :: thesis: for A', B' being RoughSet of X st A = A' & B = B' holds
( A [= B iff ( LAp A' c= LAp B' & UAp A' c= UAp B' ) )
let A', B' be RoughSet of X; :: thesis: ( A = A' & B = B' implies ( A [= B iff ( LAp A' c= LAp B' & UAp A' c= UAp B' ) ) )
assume Z1: ( A = A' & B = B' ) ; :: thesis: ( A [= B iff ( LAp A' c= LAp B' & UAp A' c= UAp B' ) )
Z2: ( A is Element of RoughSets X & B is Element of RoughSets X ) by Def8;
thus ( A [= B implies ( LAp A' c= LAp B' & UAp A' c= UAp B' ) ) :: thesis: ( LAp A' c= LAp B' & UAp A' c= UAp B' implies A [= B )

proof

assume A [= B ; :: thesis: ( LAp A' c= LAp B' & UAp A' c= UAp B' )
then A "\/" B = B by LATTICES:def 3;
then A' _\/_ B' = B' by Z1, Def8, Z2;
then ( (LAp A') \/ (LAp B') = LAp B' & (UAp A') \/ (UAp B') = UAp B' ) by Th1, Th2;
hence ( LAp A' c= LAp B' & UAp A' c= UAp B' ) by XBOOLE_1:11; :: thesis: verum

end;

assume ( LAp A' c= LAp B' & UAp A' c= UAp B' ) ; :: thesis: A [= B
then ( (LAp A') \/ (LAp B') = LAp B' & (UAp A') \/ (UAp B') = UAp B' ) by XBOOLE_1:12;
then ( LAp (A' _\/_ B') = LAp B' & UAp (A' _\/_ B') = UAp B' ) by Th1, Th2;
then A1: A' _\/_ B' = B' by Def5;
reconsider A1 = A, B1 = B as Element of RoughSets X by Def8;
reconsider A' = A1, B' = B1 as RoughSet of X by DefRSX;
A' _\/_ B' = A "\/" B by Def8;
hence A [= B by LATTICES:def 3, A1, Z1; :: thesis: verum