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