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

set G = RSLattice X;

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

set G = RSLattice X;

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