let u, v, w be Element of (RSLattice X); :: according to LATTICES:def 11 :: thesis: u "/\" (v "\/" w) = (u "/\" v) "\/" (u "/\" w)
reconsider K = u, L = v, M = w as Element of RoughSets X by Def23;
thus u "/\" (v "\/" w) = the L_join of (RSLattice X) . (( the L_meet of (RSLattice X) . (K,L)),( the L_meet of (RSLattice X) . (K,M))) by Lm12
.= (u "/\" v) "\/" (u "/\" w) ; :: thesis: verum