let L be non empty LattStr ; :: thesis: ( L is Lattice-like iff ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing ) )
A1: ( L is Lattice-like implies ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing ) )

proof

assume A2: L is Lattice-like ; :: thesis: ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing )
A3: for x, y, z being Element of L holds x "/\" (y "/\" z) = y "/\" (x "/\" z)

proof

let a, b, c be Element of L; :: thesis: a "/\" (b "/\" c) = b "/\" (a "/\" c)
a "/\" (b "/\" c) = (a "/\" b) "/\" c by A2, LATTICES:def 7
.= (b "/\" a) "/\" c by A2, LATTICES:def 6
.= b "/\" (a "/\" c) by A2, LATTICES:def 7 ;
hence a "/\" (b "/\" c) = b "/\" (a "/\" c) ; :: thesis: verum

end;

A4: for x, y being Element of L holds x "\/" (x "/\" y) = x

proof

let a, b be Element of L; :: thesis: a "\/" (a "/\" b) = a
a = (b "/\" a) "\/" a by A2, LATTICES:def 8
.= (a "/\" b) "\/" a by A2, LATTICES:def 6
.= a "\/" (a "/\" b) by A2, LATTICES:def 4 ;
hence a "\/" (a "/\" b) = a ; :: thesis: verum

end;

for x, y, z being Element of L holds x "\/" (y "\/" z) = y "\/" (x "\/" z)

proof

let a, b, c be Element of L; :: thesis: a "\/" (b "\/" c) = b "\/" (a "\/" c)
a "\/" (b "\/" c) = (a "\/" b) "\/" c by A2, LATTICES:def 5
.= (b "\/" a) "\/" c by A2, LATTICES:def 4
.= b "\/" (a "\/" c) by A2, LATTICES:def 5 ;
hence a "\/" (b "\/" c) = b "\/" (a "\/" c) ; :: thesis: verum

end;

hence ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing ) by A2, A3, A4, Def1, Def2, Def3; :: thesis: verum

end;

( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing implies L is Lattice-like )

proof

assume A5: ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing ) ; :: thesis: L is Lattice-like
then A6: L is meet-absorbing by Th3;
( L is meet-commutative & L is join-commutative & L is meet-associative & L is join-associative ) by A5, Th2, Th4;
hence L is Lattice-like by A5, A6; :: thesis: verum

end;

hence ( L is Lattice-like iff ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing ) ) by A1; :: thesis: verum