let X be Tolerance_Space; :: thesis: for a, b being Element of holds (a "/\" b) "\/" b = b
let a, b be Element of ; :: thesis: (a "/\" b) "\/" b = b
set G = RSLattice X;
reconsider a1 = a, b1 = b as Element of RoughSets X by Def8;
reconsider a' = a1, b' = b1 as RoughSet of X by DefRSX;
thus (a "/\" b) "\/" b = the L_join of (RSLattice X) . (the L_meet of (RSLattice X) . a1,b1),b1
.= b by Lm8 ; :: thesis: verum