set G = NormForm A;

thus for u, v being Element of (NormForm A) holds u "\/" v = v "\/" u by Lm9; :: according to LATTICES:def 4,LATTICES:def 10 :: thesis: ( NormForm A is join-associative & NormForm A is meet-absorbing & NormForm A is meet-commutative & NormForm A is meet-associative & NormForm A is join-absorbing )

thus for u, v, w being Element of (NormForm A) holds u "\/" (v "\/" w) = (u "\/" v) "\/" w by Lm10; :: according to LATTICES:def 5 :: thesis: ( NormForm A is meet-absorbing & NormForm A is meet-commutative & NormForm A is meet-associative & NormForm A is join-absorbing )

thus for u, v being Element of (NormForm A) holds (u "/\" v) "\/" v = v by Lm12; :: according to LATTICES:def 8 :: thesis: ( NormForm A is meet-commutative & NormForm A is meet-associative & NormForm A is join-absorbing )

thus for u, v being Element of (NormForm A) holds u "/\" v = v "/\" u by Lm13; :: according to LATTICES:def 6 :: thesis: ( NormForm A is meet-associative & NormForm A is join-absorbing )

thus for u, v, w being Element of (NormForm A) holds u "/\" (v "/\" w) = (u "/\" v) "/\" w by Lm14; :: according to LATTICES:def 7 :: thesis: NormForm A is join-absorbing

let u, v be Element of (NormForm A); :: according to LATTICES:def 9 :: thesis: u "/\" (u "\/" v) = u

thus u "/\" (u "\/" v) = u by Lm16; :: thesis: verum

thus for u, v being Element of (NormForm A) holds u "\/" v = v "\/" u by Lm9; :: according to LATTICES:def 4,LATTICES:def 10 :: thesis: ( NormForm A is join-associative & NormForm A is meet-absorbing & NormForm A is meet-commutative & NormForm A is meet-associative & NormForm A is join-absorbing )

thus for u, v, w being Element of (NormForm A) holds u "\/" (v "\/" w) = (u "\/" v) "\/" w by Lm10; :: according to LATTICES:def 5 :: thesis: ( NormForm A is meet-absorbing & NormForm A is meet-commutative & NormForm A is meet-associative & NormForm A is join-absorbing )

thus for u, v being Element of (NormForm A) holds (u "/\" v) "\/" v = v by Lm12; :: according to LATTICES:def 8 :: thesis: ( NormForm A is meet-commutative & NormForm A is meet-associative & NormForm A is join-absorbing )

thus for u, v being Element of (NormForm A) holds u "/\" v = v "/\" u by Lm13; :: according to LATTICES:def 6 :: thesis: ( NormForm A is meet-associative & NormForm A is join-absorbing )

thus for u, v, w being Element of (NormForm A) holds u "/\" (v "/\" w) = (u "/\" v) "/\" w by Lm14; :: according to LATTICES:def 7 :: thesis: NormForm A is join-absorbing

let u, v be Element of (NormForm A); :: according to LATTICES:def 9 :: thesis: u "/\" (u "\/" v) = u

thus u "/\" (u "\/" v) = u by Lm16; :: thesis: verum