let X be Tolerance_Space; :: thesis: for a, b, c being Element of (RSLattice X) holds a "/\" (b "/\" c) = (a "/\" b) "/\" c
let a, b, c be Element of (RSLattice X); :: thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c
reconsider a1 = a, b1 = b, c1 = c as Element of RoughSets X by Def23;
reconsider a9 = a1, b9 = b1, c9 = c1 as RoughSet of X by Def20;
set G = RSLattice X;
A1: b9 _/\_ c9 is Element of RoughSets X by Def20;
A2: a9 _/\_ b9 is Element of RoughSets X by Def20;
a "/\" (b "/\" c) = the L_meet of (RSLattice X) . (a1,(b9 _/\_ c9)) by Def23
.= a9 _/\_ (b9 _/\_ c9) by Def23, A1
.= (a9 _/\_ b9) _/\_ c9 by Th65
.= the L_meet of (RSLattice X) . ((a9 _/\_ b9),c1) by Def23, A2
.= (a "/\" b) "/\" c by Def23 ;
hence a "/\" (b "/\" c) = (a "/\" b) "/\" c ; :: thesis: verum