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_join of (RSLattice X) . (a,(b9 _\/_ c9)) by Def23

.= a9 _\/_ (b9 _\/_ c9) by Def23, A1

.= (a9 _\/_ b9) _\/_ c9 by Th64

.= the L_join of (RSLattice X) . ((a9 _\/_ b9),c1) by Def23, A2

.= (a "\/" b) "\/" c by Def23 ;

hence a "\/" (b "\/" c) = (a "\/" b) "\/" c ; :: thesis: verum

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_join of (RSLattice X) . (a,(b9 _\/_ c9)) by Def23

.= a9 _\/_ (b9 _\/_ c9) by Def23, A1

.= (a9 _\/_ b9) _\/_ c9 by Th64

.= the L_join of (RSLattice X) . ((a9 _\/_ b9),c1) by Def23, A2

.= (a "\/" b) "\/" c by Def23 ;

hence a "\/" (b "\/" c) = (a "\/" b) "\/" c ; :: thesis: verum