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