let X be Tolerance_Space; for K, L, M being Element of RoughSets X holds the L_meet of (RSLattice X) . K,(the L_join of (RSLattice X) . L,M) = the L_join of (RSLattice X) . (the L_meet of (RSLattice X) . K,L),(the L_meet of (RSLattice X) . K,M)
let K, L, M be Element of RoughSets X; the L_meet of (RSLattice X) . K,(the L_join of (RSLattice X) . L,M) = the L_join of (RSLattice X) . (the L_meet of (RSLattice X) . K,L),(the L_meet of (RSLattice X) . K,M)
set G = RSLattice X;
reconsider K' = K, L' = L, M' = M as RoughSet of X by DefRSX;
XX:
L' _\/_ M' is Element of RoughSets X
by DefRSX;
XY:
K' _/\_ L' is Element of RoughSets X
by DefRSX;
XQ:
K' _/\_ M' is Element of RoughSets X
by DefRSX;
the L_meet of (RSLattice X) . K,(the L_join of (RSLattice X) . L,M) =
the L_meet of (RSLattice X) . K,(L' _\/_ M')
by Def8
.=
K' _/\_ (L' _\/_ M')
by Def8, XX
.=
(K' _/\_ L') _\/_ (K' _/\_ M')
by Th9
.=
the L_join of (RSLattice X) . (K' _/\_ L'),(K' _/\_ M')
by Def8, XY, XQ
.=
the L_join of (RSLattice X) . (the L_meet of (RSLattice X) . K,L),(K' _/\_ M')
by Def8
.=
the L_join of (RSLattice X) . (the L_meet of (RSLattice X) . K,L),(the L_meet of (RSLattice X) . K,M)
by Def8
;
hence
the L_meet of (RSLattice X) . K,(the L_join of (RSLattice X) . L,M) = the L_join of (RSLattice X) . (the L_meet of (RSLattice X) . K,L),(the L_meet of (RSLattice X) . K,M)
; verum