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