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 A1: ( A = A9 & B = B9 ) ; :: thesis: ( A [= B iff ( LAp A9 c= LAp B9 & UAp A9 c= UAp B9 ) )
A2: ( A is Element of RoughSets X & B is Element of RoughSets X ) by Def23;
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 ;
then A9 _\/_ B9 = B9 by A1, Def23, A2;
then ( (LAp A9) \/ (LAp B9) = LAp B9 & (UAp A9) \/ (UAp B9) = UAp B9 ) ;
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 ) ;
then A3: A9 _\/_ B9 = B9 ;
reconsider A1 = A, B1 = B as Element of RoughSets X by Def23;
reconsider A9 = A1, B9 = B1 as RoughSet of X by Def20;
A9 _\/_ B9 = A "\/" B by Def23;
hence A [= B by A3, A1; :: thesis: verum