let X be Tolerance_Space; :: thesis: for a, b being Element of (RSLattice X) holds a "/\" (a "\/" b) = a

let a, b be Element of (RSLattice X); :: thesis: a "/\" (a "\/" b) = a

set G = RSLattice X;

reconsider a1 = a, b1 = b as Element of RoughSets X by Def23;

reconsider a9 = a1 as RoughSet of X by Def20;

thus a "/\" (a "\/" b) = the L_join of (RSLattice X) . (( the L_meet of (RSLattice X) . (a1,a1)),( the L_meet of (RSLattice X) . (a1,b1))) by Lm12

.= the L_join of (RSLattice X) . ((a9 _/\_ a9),( the L_meet of (RSLattice X) . (a1,b1))) by Def23

.= a "\/" (a "/\" b) by Th61

.= (a "/\" b) "\/" a by Lm6

.= (b "/\" a) "\/" a by Lm10

.= a by Lm9 ; :: thesis: verum

let a, b be Element of (RSLattice X); :: thesis: a "/\" (a "\/" b) = a

set G = RSLattice X;

reconsider a1 = a, b1 = b as Element of RoughSets X by Def23;

reconsider a9 = a1 as RoughSet of X by Def20;

thus a "/\" (a "\/" b) = the L_join of (RSLattice X) . (( the L_meet of (RSLattice X) . (a1,a1)),( the L_meet of (RSLattice X) . (a1,b1))) by Lm12

.= the L_join of (RSLattice X) . ((a9 _/\_ a9),( the L_meet of (RSLattice X) . (a1,b1))) by Def23

.= a "\/" (a "/\" b) by Th61

.= (a "/\" b) "\/" a by Lm6

.= (b "/\" a) "\/" a by Lm10

.= a by Lm9 ; :: thesis: verum