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

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