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 )
then A3: ( L is meet-absorbing & L is join-absorbing ) ;
A4: ( L is meet-associative & L is meet-commutative & L is join-associative & L is join-commutative ) by A2;
A5: 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 A4, LATTICES:def 5
.= (b "\/" a) "\/" c by A4, LATTICES:def 4
.= b "\/" (a "\/" c) by A4, LATTICES:def 5 ;
hence a "\/" (b "\/" c) = b "\/" (a "\/" c) ; :: thesis: verum

end;

A6: 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 A4, LATTICES:def 7
.= (b "/\" a) "/\" c by A4, LATTICES:def 6
.= b "/\" (a "/\" c) by A4, LATTICES:def 7 ;
hence a "/\" (b "/\" c) = b "/\" (a "/\" c) ; :: thesis: verum

end;

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 A3, LATTICES:def 8
.= (a "/\" b) "\/" a by A4, LATTICES:def 6
.= a "\/" (a "/\" b) by A4, LATTICES:def 4 ;
hence a "\/" (a "/\" b) = a ; :: thesis: verum

end;

hence ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing ) by A2, A5, A6, 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 A7: ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing ) ; :: thesis: L is Lattice-like
then A8: ( L is meet-commutative & L is join-commutative ) by Th2;
A9: ( L is meet-associative & L is join-associative ) by A7, Th4;
L is meet-absorbing by A7, Th3;
hence L is Lattice-like by A7, A8, A9; :: 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