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 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))) ; :: thesis: verum