set G = SubstLatt (V,C);
thus for u, v being Element of (SubstLatt (V,C)) holds u "\/" v = v "\/" u by Lm5; :: 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 Lm6; :: 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 Lm8; :: 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 Lm9; :: 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 Lm10; :: 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 Lm12; :: thesis: verum