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 K9 = K, L9 = L, M9 = M as RoughSet of X by Def20;
A1:
L9 _\/_ M9 is Element of RoughSets X
by Def20;
A2:
K9 _/\_ L9 is Element of RoughSets X
by Def20;
A3:
K9 _/\_ M9 is Element of RoughSets X
by Def20;
the L_meet of (RSLattice X) . (K,( the L_join of (RSLattice X) . (L,M))) =
the L_meet of (RSLattice X) . (K,(L9 _\/_ M9))
by Def23
.=
K9 _/\_ (L9 _\/_ M9)
by Def23, A1
.=
(K9 _/\_ L9) _\/_ (K9 _/\_ M9)
by Th66
.=
the L_join of (RSLattice X) . ((K9 _/\_ L9),(K9 _/\_ M9))
by Def23, A2, A3
.=
the L_join of (RSLattice X) . (( the L_meet of (RSLattice X) . (K,L)),(K9 _/\_ M9))
by Def23
.=
the L_join of (RSLattice X) . (( the L_meet of (RSLattice X) . (K,L)),( the L_meet of (RSLattice X) . (K,M)))
by Def23
;
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