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