let X be Tolerance_Space; :: thesis: for a, b being Element of holds a "/\" b = b "/\" a
set G = RSLattice X;
let a, b be Element of ; :: thesis: a "/\" b = b "/\" a
reconsider a1 = a, b1 = b as Element of RoughSets X by Def8;
reconsider a' = a1, b' = b1 as RoughSet of X by DefRSX;
a "/\" b = a' _/\_ b' by Def8
.= b' _/\_ a'
.= b "/\" a by Def8 ;
hence a "/\" b = b "/\" a ; :: thesis: verum