let L be non empty LattStr ; :: thesis: ( L = RealFunc_Lattice A implies ( L is join-commutative & L is join-associative & L is meet-absorbing & L is meet-commutative & L is meet-associative & L is join-absorbing ) )
assume A1: L = RealFunc_Lattice A ; :: thesis: ( L is join-commutative & L is join-associative & L is meet-absorbing & L is meet-commutative & L is meet-associative & L is join-absorbing )
thus for p, q being Element of L holds p "\/" q = q "\/" p by Th8, A1; :: according to LATTICES:def 4 :: thesis: ( L is join-associative & L is meet-absorbing & L is meet-commutative & L is meet-associative & L is join-absorbing )
thus for p, q, r being Element of L holds p "\/" (q "\/" r) = (p "\/" q) "\/" r by Th10, A1; :: according to LATTICES:def 5 :: thesis: ( L is meet-absorbing & L is meet-commutative & L is meet-associative & L is join-absorbing )
thus for p, q being Element of L holds (p "/\" q) "\/" q = q by Th14, A1; :: according to LATTICES:def 8 :: thesis: ( L is meet-commutative & L is meet-associative & L is join-absorbing )
thus for p, q being Element of L holds p "/\" q = q "/\" p by Th9, A1; :: according to LATTICES:def 6 :: thesis: ( L is meet-associative & L is join-absorbing )
thus for p, q, r being Element of L holds p "/\" (q "/\" r) = (p "/\" q) "/\" r by Th11, A1; :: according to LATTICES:def 7 :: thesis: L is join-absorbing
thus for p, q being Element of L holds p "/\" (p "\/" q) = p by Th16, A1; :: according to LATTICES:def 9 :: thesis: verum