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

proof

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

end;

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