let L be non empty LattStr ; ( ( 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 )
assume A1:
for v1, v0 being Element of L holds v0 "/\" v1 = v1 "/\" v0
; ( ex v0, v2, v1 being Element of L st not (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) or ex v0 being Element of L st not v0 "\/" v0 = v0 or ex v2, v1, v0 being Element of L st not (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) or ex v1, v0 being Element of L st not v0 "\/" v1 = v1 "\/" v0 or ex v0, v2, v1 being Element of L st not (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) or ex v2, v1, v0 being Element of L st not (v0 "/\" v1) "\/" (v0 "/\" v2) = v0 "/\" (v1 "\/" (v0 "/\" v2)) or for v1, v2, v3 being Element of L st v1 "\/" v2 = v2 holds
v1 "\/" (v3 "/\" v2) = (v1 "\/" v3) "/\" v2 )
assume A2:
for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2)
; ( ex v0 being Element of L st not v0 "\/" v0 = v0 or ex v2, v1, v0 being Element of L st not (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) or ex v1, v0 being Element of L st not v0 "\/" v1 = v1 "\/" v0 or ex v0, v2, v1 being Element of L st not (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) or ex v2, v1, v0 being Element of L st not (v0 "/\" v1) "\/" (v0 "/\" v2) = v0 "/\" (v1 "\/" (v0 "/\" v2)) or for v1, v2, v3 being Element of L st v1 "\/" v2 = v2 holds
v1 "\/" (v3 "/\" v2) = (v1 "\/" v3) "/\" v2 )
assume A3:
for v0 being Element of L holds v0 "\/" v0 = v0
; ( ex v2, v1, v0 being Element of L st not (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) or ex v1, v0 being Element of L st not v0 "\/" v1 = v1 "\/" v0 or ex v0, v2, v1 being Element of L st not (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) or ex v2, v1, v0 being Element of L st not (v0 "/\" v1) "\/" (v0 "/\" v2) = v0 "/\" (v1 "\/" (v0 "/\" v2)) or for v1, v2, v3 being Element of L st v1 "\/" v2 = v2 holds
v1 "\/" (v3 "/\" v2) = (v1 "\/" v3) "/\" v2 )
assume A4:
for v2, v1, v0 being Element of L holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2)
; ( ex v1, v0 being Element of L st not v0 "\/" v1 = v1 "\/" v0 or ex v0, v2, v1 being Element of L st not (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) or ex v2, v1, v0 being Element of L st not (v0 "/\" v1) "\/" (v0 "/\" v2) = v0 "/\" (v1 "\/" (v0 "/\" v2)) or for v1, v2, v3 being Element of L st v1 "\/" v2 = v2 holds
v1 "\/" (v3 "/\" v2) = (v1 "\/" v3) "/\" v2 )
assume A5:
for v1, v0 being Element of L holds v0 "\/" v1 = v1 "\/" v0
; ( ex v0, v2, v1 being Element of L st not (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) or ex v2, v1, v0 being Element of L st not (v0 "/\" v1) "\/" (v0 "/\" v2) = v0 "/\" (v1 "\/" (v0 "/\" v2)) or for v1, v2, v3 being Element of L st v1 "\/" v2 = v2 holds
v1 "\/" (v3 "/\" v2) = (v1 "\/" v3) "/\" v2 )
assume A6:
for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2)
; ( ex v2, v1, v0 being Element of L st not (v0 "/\" v1) "\/" (v0 "/\" v2) = v0 "/\" (v1 "\/" (v0 "/\" v2)) or for v1, v2, v3 being Element of L st v1 "\/" v2 = v2 holds
v1 "\/" (v3 "/\" v2) = (v1 "\/" v3) "/\" v2 )
A8:
for v0, v2, v1 being Element of L holds (v0 "\/" v1) "/\" (v0 "\/" (v1 "/\" v2)) = v0 "\/" (v1 "/\" v2)
assume A9:
for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" v2) = v0 "/\" (v1 "\/" (v0 "/\" v2))
; for v1, v2, v3 being Element of L st v1 "\/" v2 = v2 holds
v1 "\/" (v3 "/\" v2) = (v1 "\/" v3) "/\" v2
assume
ex v1, v2, v3 being Element of L st
( v1 "\/" v2 = v2 & not v1 "\/" (v3 "/\" v2) = (v1 "\/" v3) "/\" v2 )
; contradiction
then consider c1, c2, c3 being Element of L such that
A10:
c1 "\/" c2 = c2
and
A11:
c1 "\/" (c3 "/\" c2) <> (c1 "\/" c3) "/\" c2
;
c1 "\/" (c2 "/\" c3) <> (c1 "\/" c3) "/\" c2
by A1, A11;
then A15:
c1 "\/" (c2 "/\" c3) <> c2 "/\" (c1 "\/" c3)
by A1;
A17:
for v0, v2, v1 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" (v1 "\/" v2)) = v0 "/\" (v1 "\/" v2)
A19:
for v0, v2, v1 being Element of L holds v0 "/\" (v1 "\/" (v0 "/\" (v1 "\/" v2))) = v0 "/\" (v1 "\/" v2)
A22:
for v102, v101 being Element of L holds v101 "\/" v102 = v101 "\/" (v101 "\/" v102)
A27:
for v1, v2, v0 being Element of L holds v0 "/\" (v1 "\/" (v0 "/\" v2)) = (v0 "/\" v2) "\/" (v0 "/\" v1)
A29:
for v1, v2, v0 being Element of L holds v0 "/\" (v1 "\/" (v0 "/\" v2)) = v0 "/\" (v2 "\/" (v0 "/\" v1))
A35:
for v102 being Element of L holds c1 "\/" (c2 "/\" (c1 "\/" v102)) = c2 "/\" (c1 "\/" v102)
A38:
for v0 being Element of L holds c1 "\/" (c2 "/\" (v0 "\/" c1)) = c2 "/\" (c1 "\/" v0)
A40:
for v0, v2, v1 being Element of L holds v0 "/\" ((v1 "\/" v2) "\/" (v0 "/\" v1)) = v0 "/\" (v1 "\/" v2)
A42:
for v2, v1, v0 being Element of L holds v0 "/\" (v1 "\/" (v2 "\/" (v0 "/\" v1))) = v0 "/\" (v1 "\/" v2)
A44:
for v0 being Element of L holds c2 "/\" (v0 "\/" (c2 "/\" c1)) = c1 "\/" (c2 "/\" v0)
A45:
c2 "/\" c1 = c1 "/\" c2
by A1;
A50:
for v101 being Element of L holds c2 "/\" (v101 "\/" (c1 "\/" (c2 "/\" v101))) = c2 "/\" (v101 "\/" (c1 "/\" c2))
A53:
for v0 being Element of L holds c2 "/\" (v0 "\/" c1) = c2 "/\" (v0 "\/" (c1 "/\" c2))
A57:
for v0 being Element of L holds c1 "\/" (c2 "/\" (v0 "\/" (c1 "/\" c2))) = c1 "\/" (c2 "/\" v0)
A59:
for v0 being Element of L holds c1 "\/" (c2 "/\" (v0 "\/" c1)) = c1 "\/" (c2 "/\" v0)
for v0 being Element of L holds c2 "/\" (c1 "\/" v0) = c1 "\/" (c2 "/\" v0)
hence
contradiction
by A15; verum