let L be non empty LattStr ; :: thesis: ( the L_join of L is commutative & the L_join of L is associative & the L_meet of L is commutative & the L_meet of L is associative & the L_join of L absorbs the L_meet of L & the L_meet of L absorbs the L_join of L implies L is Lattice-like )
assume that
A1: the L_join of L is commutative and
A2: the L_join of L is associative and
A3: the L_meet of L is commutative and
A4: the L_meet of L is associative and
A5: the L_join of L absorbs the L_meet of L and
A6: the L_meet of L absorbs the L_join of L ; :: thesis: L is Lattice-like
thus for a, b being Element of L holds a "\/" b = b "\/" a by A1; :: according to LATTICES:def 4,LATTICES:def 10 :: thesis: ( L is join-associative & L is meet-absorbing & L is meet-commutative & L is meet-associative & L is join-absorbing )
thus for a, b, c being Element of L holds a "\/" (b "\/" c) = (a "\/" b) "\/" c by A2; :: according to LATTICES:def 5 :: thesis: ( L is meet-absorbing & L is meet-commutative & L is meet-associative & L is join-absorbing )
thus for a, b being Element of L holds (a "/\" b) "\/" b = b :: according to LATTICES:def 8 :: thesis: ( L is meet-commutative & L is meet-associative & L is join-absorbing ) thus for a, b being Element of L holds a "/\" b = b "/\" a by A3; :: according to LATTICES:def 6 :: thesis: ( L is meet-associative & L is join-absorbing )
thus for a, b, c being Element of L holds a "/\" (b "/\" c) = (a "/\" b) "/\" c by A4; :: according to LATTICES:def 7 :: thesis: L is join-absorbing
let a be Element of L; :: according to LATTICES:def 9 :: thesis: for b₁ being Element of the carrier of L holds a "/\" (a "\/" b₁) = a
let b be Element of L; :: thesis: a "/\" (a "\/" b) = a
thus a "/\" (a "\/" b) = a by A6; :: thesis: verum