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 K' = K, L' = L as RoughSet of X by DefRSX;
A1: K' _/\_ L' 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) . (K' _/\_ L'),L by Def8
.= (K' _/\_ L') _\/_ L' by Def8, A1
.= L' _\/_ (L' _/\_ K')
.= L by Th10 ; :: thesis: verum