let X be Tolerance_Space; :: thesis: for a, b being Element of (RSLattice X) holds a "/\" (a "\/" b) = a
let a, b be Element of (RSLattice X); :: thesis: a "/\" (a "\/" b) = a
set G = RSLattice X;
reconsider a1 = a, b1 = b as Element of RoughSets X by Def23;
reconsider a9 = a1 as RoughSet of X by Def20;
thus a "/\" (a "\/" b) = the L_join of (RSLattice X) . (( the L_meet of (RSLattice X) . (a1,a1)),( the L_meet of (RSLattice X) . (a1,b1))) by Lm12
.= the L_join of (RSLattice X) . ((a9 _/\_ a9),( the L_meet of (RSLattice X) . (a1,b1))) by Def23
.= a "\/" (a "/\" b) by Th61
.= (a "/\" b) "\/" a by Lm6
.= (b "/\" a) "\/" a by Lm10
.= a by Lm9 ; :: thesis: verum