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 by LATTICES:def 3;
then A9 _\/_ B9 = B9 by A1, Def23, A2;
then ( (LAp A9) \/ (LAp B9) = LAp B9 & (UAp A9) \/ (UAp B9) = UAp B9 ) by Th56, Th57;
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 Th56, Th57;
then A3: A9 _\/_ B9 = B9 by Def17;
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, LATTICES:def 3; :: thesis: verum