let X be Tolerance_Space; :: thesis: 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; :: thesis: 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 DefRSX;
XX: L9 _\/_ M9 is Element of RoughSets X by DefRSX;
XY: K9 _/\_ L9 is Element of RoughSets X by DefRSX;
XQ: K9 _/\_ M9 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,(L9 _\/_ M9)) by Def8
.= K9 _/\_ (L9 _\/_ M9) by Def8, XX
.= (K9 _/\_ L9) _\/_ (K9 _/\_ M9) by Th9
.= the L_join of (RSLattice X) . ((K9 _/\_ L9),(K9 _/\_ M9)) by Def8, XY, XQ
.= the L_join of (RSLattice X) . (( the L_meet of (RSLattice X) . (K,L)),(K9 _/\_ M9)) 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))) ; :: thesis: verum