let X be Tolerance_Space; :: thesis: for K, L being Element of RoughSets X holds the L_join of (RSLattice X) . (( the L_meet of (RSLattice X) . (K,L)),L) = L
let K, L be Element of RoughSets X; :: thesis: the L_join of (RSLattice X) . (( the L_meet of (RSLattice X) . (K,L)),L) = L
reconsider K9 = K, L9 = L as RoughSet of X by Def20;
A1: K9 _/\_ L9 is Element of RoughSets X by Def20;
thus the L_join of (RSLattice X) . (( the L_meet of (RSLattice X) . (K,L)),L) = the L_join of (RSLattice X) . ((K9 _/\_ L9),L) by Def23
.= (K9 _/\_ L9) _\/_ L9 by Def23, A1
.= L9 _\/_ (L9 _/\_ K9)
.= L by Th67 ; :: thesis: verum