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

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