let X be Tolerance_Space; :: thesis: for a, b being Element of (RSLattice X) holds a "/\" b = b "/\" a
let a, b be Element of (RSLattice X); :: thesis: a "/\" b = b "/\" a
reconsider a1 = a, b1 = b as Element of RoughSets X by Def23;
reconsider a9 = a1, b9 = b1 as RoughSet of X by Def20;
a "/\" b = a9 _/\_ b9 by Def23
.= b9 _/\_ a9
.= b "/\" a by Def23 ;
hence a "/\" b = b "/\" a ; :: thesis: verum