let L be non empty LattStr ; :: thesis: ( L is Lattice iff L is satisfying_4_McKenzie_axioms )
thus ( L is Lattice implies L is satisfying_4_McKenzie_axioms ) :: thesis: ( L is satisfying_4_McKenzie_axioms implies L is Lattice )

proof

assume A1: L is Lattice ; :: thesis: L is satisfying_4_McKenzie_axioms
C1: for v1, v0 being Element of L holds v0 "/\" (v0 "\/" v1) = v0 by A1, LATTICES:def 9;
for v1, v0 being Element of L holds v0 "\/" (v0 "/\" v1) = v0

proof

let v1, v0 be Element of L; :: thesis: v0 "\/" (v0 "/\" v1) = v0
A2: ( L is join-commutative & L is meet-commutative & L is meet-absorbing ) by A1;
then v0 "\/" (v0 "/\" v1) = (v0 "/\" v1) "\/" v0
.= (v1 "/\" v0) "\/" v0 by A2
.= v0 by A2 ;
hence v0 "\/" (v0 "/\" v1) = v0 ; :: thesis: verum

end;

then ( L is satisfying_McKenzie_1 & L is satisfying_McKenzie_2 & L is satisfying_McKenzie_3 & L is satisfying_McKenzie_4 ) by AuxiliaryMcKenzie, A1, C1;
hence L is satisfying_4_McKenzie_axioms ; :: thesis: verum

end;

assume L is satisfying_4_McKenzie_axioms ; :: thesis: L is Lattice
then b1: ( L is satisfying_McKenzie_1 & L is satisfying_McKenzie_2 & L is satisfying_McKenzie_3 & L is satisfying_McKenzie_4 ) ;
then B1: ( ( for v1, v0 being Element of L holds v0 "/\" (v0 "\/" v1) = v0 ) & ( for v1, v0 being Element of L holds v0 "\/" (v0 "/\" v1) = v0 ) & L is join-commutative & L is meet-commutative & L is meet-associative & L is join-associative ) by MainMcKenzie;
B2: for v0, v1 being Element of L holds (v1 "/\" v0) "\/" v0 = v0

proof

let v0, v1 be Element of L; :: thesis: (v1 "/\" v0) "\/" v0 = v0
(v1 "/\" v0) "\/" v0 = v0 "\/" (v1 "/\" v0) by B1
.= v0 "\/" (v0 "/\" v1) by B1
.= v0 by b1, MainMcKenzie ;
hence (v1 "/\" v0) "\/" v0 = v0 ; :: thesis: verum

end;

( L is meet-absorbing & L is join-absorbing ) by b1, B2, MainMcKenzie;
hence L is Lattice by B1; :: thesis: verum