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