let X be Tolerance_Space; :: thesis: for a, b, c being Element of holds a "/\" (b "/\" c) = (a "/\" b) "/\" c
let a, b, c be Element of ; :: thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c
reconsider a1 = a, b1 = b, c1 = c as Element of RoughSets X by Def8;
reconsider a' = a1, b' = b1, c' = c1 as RoughSet of X by DefRSX;
set G = RSLattice X;
XX: b' _/\_ c' is Element of RoughSets X by DefRSX;
XY: a' _/\_ b' is Element of RoughSets X by DefRSX;
a "/\" (b "/\" c) = the L_meet of (RSLattice X) . a1,(b' _/\_ c') by Def8
.= a' _/\_ (b' _/\_ c') by Def8, XX
.= (a' _/\_ b') _/\_ c' by Th8
.= the L_meet of (RSLattice X) . (a' _/\_ b'),c1 by Def8, XY
.= (a "/\" b) "/\" c by Def8 ;
hence a "/\" (b "/\" c) = (a "/\" b) "/\" c ; :: thesis: verum