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