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 Def8;
reconsider a9 = a1, b9 = b1 as RoughSet of X by DefRSX;
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 Def8
.= a "\/" (a "/\" b) by Th21
.= (a "/\" b) "\/" a by Lm6
.= (b "/\" a) "\/" a by Lm10
.= a by Lm9 ; :: thesis: verum