:: deftheorem Def23 defines RSLattice INTERVA1:def 23 :
for X being Tolerance_Space
for b₂ being strict LattStr holds
( b₂ = RSLattice X iff ( the carrier of b₂ = RoughSets X & ( for A, B being Element of RoughSets X
for A9, B9 being RoughSet of X st A = A9 & B = B9 holds
( the L_join of b₂ . (A,B) = A9 _\/_ B9 & the L_meet of b₂ . (A,B) = A9 _/\_ B9 ) ) ) );