set G = RSLattice X;
thus for u, v being Element of (RSLattice X) holds u "\/" v = v "\/" u by Lm6; :: according to LATTICES:def 4,LATTICES:def 10 :: thesis: ( RSLattice X is join-associative & RSLattice X is meet-absorbing & RSLattice X is meet-commutative & RSLattice X is meet-associative & RSLattice X is join-absorbing )
thus for u, v, w being Element of (RSLattice X) holds u "\/" (v "\/" w) = (u "\/" v) "\/" w by Lm7; :: according to LATTICES:def 5 :: thesis: ( RSLattice X is meet-absorbing & RSLattice X is meet-commutative & RSLattice X is meet-associative & RSLattice X is join-absorbing )
thus for u, v being Element of (RSLattice X) holds (u "/\" v) "\/" v = v by Lm9; :: according to LATTICES:def 8 :: thesis: ( RSLattice X is meet-commutative & RSLattice X is meet-associative & RSLattice X is join-absorbing )
thus for u, v being Element of (RSLattice X) holds u "/\" v = v "/\" u by Lm10; :: according to LATTICES:def 6 :: thesis: ( RSLattice X is meet-associative & RSLattice X is join-absorbing )
thus for u, v, w being Element of (RSLattice X) holds u "/\" (v "/\" w) = (u "/\" v) "/\" w by Lm11; :: according to LATTICES:def 7 :: thesis: RSLattice X is join-absorbing
let u, v be Element of (RSLattice X); :: according to LATTICES:def 9 :: thesis: u "/\" (u "\/" v) = u
thus u "/\" (u "\/" v) = u by Lm13; :: thesis: verum