let X be Tolerance_Space; 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; 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
; verum