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 DefRSX;
A1: K9 _/\_ L9 is Element of RoughSets X by DefRSX;
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 Def8
.= (K9 _/\_ L9) _\/_ L9 by Def8, A1
.= L9 _\/_ (L9 _/\_ K9)
.= L by Th10 ; :: thesis: verum