let L be non empty LattStr ; :: thesis: ( L is meet-idempotent & L is join-idempotent & L is meet-commutative & L is join-commutative & L is meet-associative & L is join-associative & L is satisfying_QLT1 & L is satisfying_QLT2 & ( for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" v2) = v0 "/\" (v1 "\/" (v0 "/\" v2)) ) implies L is modular )

assume A0: ( L is meet-idempotent & L is join-idempotent & L is meet-commutative & L is join-commutative & L is meet-associative & L is join-associative & L is satisfying_QLT1 & L is satisfying_QLT2 ) ; :: thesis: ( ex v2, v1, v0 being Element of L st not (v0 "/\" v1) "\/" (v0 "/\" v2) = v0 "/\" (v1 "\/" (v0 "/\" v2)) or L is modular )

A1: ( ( for v1, v0 being Element of L holds v0 "/\" v1 = v1 "/\" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) ) & ( for v0 being Element of L holds v0 "\/" v0 = v0 ) & ( for v2, v1, v0 being Element of L holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) ) & ( for v1, v0 being Element of L holds v0 "\/" v1 = v1 "\/" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) ) & ( for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" v2) = v0 "/\" (v1 "\/" (v0 "/\" v2)) ) implies for v1, v2, v3 being Element of L st v1 "\/" v2 = v2 holds

v1 "\/" (v3 "/\" v2) = (v1 "\/" v3) "/\" v2 ) by QLTMod2;

assume AA: for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" v2) = v0 "/\" (v1 "\/" (v0 "/\" v2)) ; :: thesis: L is modular

for a, b, c being Element of L st a [= c holds

a "\/" (b "/\" c) = (a "\/" b) "/\" c

assume A0: ( L is meet-idempotent & L is join-idempotent & L is meet-commutative & L is join-commutative & L is meet-associative & L is join-associative & L is satisfying_QLT1 & L is satisfying_QLT2 ) ; :: thesis: ( ex v2, v1, v0 being Element of L st not (v0 "/\" v1) "\/" (v0 "/\" v2) = v0 "/\" (v1 "\/" (v0 "/\" v2)) or L is modular )

A1: ( ( for v1, v0 being Element of L holds v0 "/\" v1 = v1 "/\" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) ) & ( for v0 being Element of L holds v0 "\/" v0 = v0 ) & ( for v2, v1, v0 being Element of L holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) ) & ( for v1, v0 being Element of L holds v0 "\/" v1 = v1 "\/" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) ) & ( for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" v2) = v0 "/\" (v1 "\/" (v0 "/\" v2)) ) implies for v1, v2, v3 being Element of L st v1 "\/" v2 = v2 holds

v1 "\/" (v3 "/\" v2) = (v1 "\/" v3) "/\" v2 ) by QLTMod2;

assume AA: for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" v2) = v0 "/\" (v1 "\/" (v0 "/\" v2)) ; :: thesis: L is modular

for a, b, c being Element of L st a [= c holds

a "\/" (b "/\" c) = (a "\/" b) "/\" c

proof

hence
L is modular
by LATTICES:def 12; :: thesis: verum
let a, b, c be Element of L; :: thesis: ( a [= c implies a "\/" (b "/\" c) = (a "\/" b) "/\" c )

assume a [= c ; :: thesis: a "\/" (b "/\" c) = (a "\/" b) "/\" c

then a "\/" c = c by LATTICES:def 3;

hence a "\/" (b "/\" c) = (a "\/" b) "/\" c by A1, AA, A0, LATTICES:def 4, LATTICES:def 5, LATTICES:def 6, ROBBINS1:def 7; :: thesis: verum

end;assume a [= c ; :: thesis: a "\/" (b "/\" c) = (a "\/" b) "/\" c

then a "\/" c = c by LATTICES:def 3;

hence a "\/" (b "/\" c) = (a "\/" b) "/\" c by A1, AA, A0, LATTICES:def 4, LATTICES:def 5, LATTICES:def 6, ROBBINS1:def 7; :: thesis: verum