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

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

set G = RSLattice X;

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

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

.= b by Lm8 ; :: thesis: verum

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

set G = RSLattice X;

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

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

.= b by Lm8 ; :: thesis: verum