theorem QLTMod:
for
L being non
empty LattStr st ( 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
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
v0,
v1,
v2 being
Element of
L st
v0 "\/" v1 = v1 holds
v0 "\/" (v2 "/\" v1) = (v0 "\/" v2) "/\" v1 ) holds
for
v1,
v2,
v3 being
Element of
L holds
(v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3))