let L be non empty LattStr ; :: thesis: ( L is distributive Lattice iff ( L is join-absorbing & L is satisfying_Sholander_1 ) )
thus ( L is distributive Lattice implies ( L is join-absorbing & L is satisfying_Sholander_1 ) ) by LatToSho; :: thesis: ( L is join-absorbing & L is satisfying_Sholander_1 implies L is distributive Lattice )
assume A1: ( L is join-absorbing & L is satisfying_Sholander_1 ) ; :: thesis: L is distributive Lattice
then A2: for v0, v2, v1 being Element of L holds v0 "/\" (v1 "\/" v2) = (v2 "/\" v0) "\/" (v1 "/\" v0) ;
then A3: L is distributive by Seventh, A1;
A4: ( L is meet-commutative & L is join-commutative ) by A2, A1, MeetCom, JoinCom;
A5: ( L is meet-associative & L is join-associative ) by A2, A1, MeetAssoc, JoinAssoc;
for v0, v1 being Element of L holds (v0 "/\" v1) "\/" v1 = v1
proof
let v0, v1 be Element of L; :: thesis: (v0 "/\" v1) "\/" v1 = v1
(v0 "/\" v1) "\/" v1 = v1 "\/" (v0 "/\" v1) by A4
.= v1 "\/" (v1 "/\" v0) by A4
.= v1 by MeetAbsor, A1, A2 ;
hence (v0 "/\" v1) "\/" v1 = v1 ; :: thesis: verum
end;
then L is meet-absorbing ;
hence L is distributive Lattice by A3, A4, A5, A1; :: thesis: verum