let L be non empty LattStr ; ( ( 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 "\/" v1) "/\" v0) "\/" v1 ) implies for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) )
assume A2:
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 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) "/\" v2) "\/" v1 = ((v2 "\/" v1) "/\" v0) "\/" v1 or for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) )
assume A3:
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 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) "/\" v2) "\/" v1 = ((v2 "\/" v1) "/\" v0) "\/" v1 or for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) )
assume A4:
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) "/\" v2) "\/" v1 = ((v2 "\/" v1) "/\" v0) "\/" v1 or for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) )
assume A5:
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) "/\" v2) "\/" v1 = ((v2 "\/" v1) "/\" v0) "\/" v1 or for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) )
assume A6:
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) "/\" v2) "\/" v1 = ((v2 "\/" v1) "/\" v0) "\/" v1 or for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) )
assume A7:
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) "/\" v2) "\/" v1 = ((v2 "\/" v1) "/\" v0) "\/" v1 or for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) )
assume A8:
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) "/\" v2) "\/" v1 = ((v2 "\/" v1) "/\" v0) "\/" v1 or for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) )
assume A9:
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) "/\" v2) "\/" v1 = ((v2 "\/" v1) "/\" v0) "\/" v1 or for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) )
A11:
for v0, v2, v1 being Element of L holds (v0 "\/" v1) "/\" (v0 "\/" (v1 "/\" v2)) = v0 "\/" (v1 "/\" v2)
assume A12:
for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" v2) "\/" v1 = ((v2 "\/" v1) "/\" v0) "\/" v1
; for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3))
A14:
for v2, v1, v0 being Element of L holds v1 "\/" ((v0 "\/" v1) "/\" v2) = ((v2 "\/" v1) "/\" v0) "\/" v1
A17:
for v2, v0, v1 being Element of L holds v0 "\/" ((v1 "\/" v0) "/\" v2) = v0 "\/" ((v2 "\/" v0) "/\" v1)
A21:
for v0, v2, v1 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" (v1 "\/" v2)) = v0 "/\" (v1 "\/" v2)
A24:
for v102, v101 being Element of L holds v101 "/\" v102 = v101 "/\" (v101 "/\" v102)
A28:
for v2, v0, v1 being Element of L holds (v1 "/\" v0) "/\" v2 = v0 "/\" (v1 "/\" v2)
A31:
for v0, v2, v1 being Element of L holds v0 "/\" (v1 "/\" v2) = v1 "/\" (v0 "/\" v2)
A34:
for v102, v100 being Element of L holds (v100 "\/" v102) "\/" v102 = v100 "\/" v102
A37:
for v1, v0 being Element of L holds v1 "\/" (v0 "\/" v1) = v0 "\/" v1
A40:
for v0, v1, v2 being Element of L holds (v0 "\/" v1) "/\" (v0 "\/" (v2 "/\" v1)) = v0 "\/" (v1 "/\" v2)
A43:
for v100, v101 being Element of L holds v100 "\/" (v101 "\/" v100) = v100 "\/" (((v101 "\/" v100) "\/" v100) "/\" v101)
A46:
for v0, v1 being Element of L holds v1 "\/" v0 = v0 "\/" (((v1 "\/" v0) "\/" v0) "/\" v1)
A49:
for v1, v0 being Element of L holds v0 "\/" v1 = v1 "\/" ((v1 "\/" (v0 "\/" v1)) "/\" v0)
A51:
for v1, v0 being Element of L holds v0 "\/" v1 = v1 "\/" ((v0 "\/" v1) "/\" v0)
A53:
for v1, v0 being Element of L holds v0 "\/" v1 = v1 "\/" (v0 "/\" (v0 "\/" v1))
A57:
for v2, v0, v1 being Element of L holds v0 "\/" (v2 "/\" (v1 "\/" v0)) = v0 "\/" ((v2 "\/" v0) "/\" v1)
A62:
for v102, v100 being Element of L holds v100 "\/" (v100 "/\" v102) = v100 "\/" ((v102 "\/" v100) "/\" v100)
A65:
for v1, v0 being Element of L holds v0 "\/" (v0 "/\" v1) = v0 "\/" (v0 "/\" (v1 "\/" v0))
A69:
for v102, v2, v100, v1 being Element of L holds (v100 "\/" ((v2 "\/" v100) "/\" v1)) "/\" (v100 "\/" (((v1 "\/" v100) "/\" v2) "/\" v102)) = v100 "\/" (((v1 "\/" v100) "/\" v2) "/\" v102)
A72:
for v3, v1, v0, v2 being Element of L holds (v0 "\/" (v1 "/\" (v2 "\/" v0))) "/\" (v0 "\/" (((v2 "\/" v0) "/\" v1) "/\" v3)) = v0 "\/" (((v2 "\/" v0) "/\" v1) "/\" v3)
A74:
for v1, v3, v0, v2 being Element of L holds (v0 "\/" (v1 "/\" (v2 "\/" v0))) "/\" (v0 "\/" ((v2 "\/" v0) "/\" (v1 "/\" v3))) = v0 "\/" (((v2 "\/" v0) "/\" v1) "/\" v3)
A76:
for v2, v0, v3, v1 being Element of L holds (v0 "\/" (v1 "/\" (v2 "\/" v0))) "/\" (v0 "\/" (v2 "/\" ((v1 "/\" v3) "\/" v0))) = v0 "\/" (((v2 "\/" v0) "/\" v1) "/\" v3)
A78:
for v2, v0, v3, v1 being Element of L holds (v0 "\/" (v1 "/\" (v2 "\/" v0))) "/\" (v0 "\/" (v2 "/\" ((v1 "/\" v3) "\/" v0))) = v0 "\/" ((v2 "\/" v0) "/\" (v1 "/\" v3))
A80:
for v2, v0, v3, v1 being Element of L holds (v0 "\/" (v1 "/\" (v2 "\/" v0))) "/\" (v0 "\/" (v2 "/\" ((v1 "/\" v3) "\/" v0))) = v0 "\/" (v2 "/\" ((v1 "/\" v3) "\/" v0))
A83:
for v102, v101 being Element of L holds v101 "\/" (v101 "/\" (v101 "\/" v102)) = v101 "/\" (v101 "\/" v102)
A87:
for v100, v101, v1 being Element of L holds (v100 "/\" v101) "\/" (v100 "/\" (v1 "\/" v101)) = v100 "/\" (v101 "\/" (v1 "\/" v101))
A90:
for v0, v1, v2 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" (v2 "\/" v1)) = v0 "/\" (v2 "\/" v1)
A93:
for v101, v1 being Element of L holds (v1 "\/" v101) "\/" (v101 "/\" (v1 "\/" v101)) = v101 "\/" (v1 "\/" v101)
A96:
for v1, v0 being Element of L holds v0 "\/" (v1 "\/" (v1 "/\" (v0 "\/" v1))) = v1 "\/" (v0 "\/" v1)
A98:
for v0, v1 being Element of L holds v0 "\/" (v1 "\/" (v1 "/\" v0)) = v1 "\/" (v0 "\/" v1)
A100:
for v0, v1 being Element of L holds v0 "\/" (v1 "\/" (v1 "/\" v0)) = v0 "\/" v1
A103:
for v0, v100, v1 being Element of L holds v100 "\/" ((v0 "/\" v1) "\/" (v0 "/\" (v1 "/\" v100))) = v100 "\/" (v0 "/\" v1)
A106:
for v1, v0 being Element of L holds v0 "\/" (v0 "/\" (v0 "\/" v1)) = v0 "\/" (v0 "/\" v1)
A108:
for v1, v0 being Element of L holds v0 "/\" (v0 "\/" v1) = v0 "\/" (v0 "/\" v1)
A111:
for v100, v1, v101 being Element of L holds v100 "/\" (v101 "\/" (v101 "/\" v1)) = v101 "/\" (v100 "/\" (v101 "\/" v1))
A115:
for v1, v100, v101 being Element of L holds (v100 "\/" v101) "/\" (v100 "\/" (v1 "/\" (v101 "\/" v100))) = v100 "\/" (v101 "/\" (v1 "\/" v100))
A119:
for v102, v1, v100 being Element of L holds (v100 "/\" v1) "\/" (v100 "/\" (v102 "\/" (v100 "/\" v1))) = v100 "/\" (v102 "\/" (v100 "/\" v1))
A123:
for v100, v103, v101 being Element of L holds (v100 "\/" (v101 "/\" ((v101 "/\" v103) "\/" v100))) "/\" (v100 "\/" ((v101 "/\" v103) "\/" ((v101 "/\" v103) "/\" v100))) = v100 "\/" ((v101 "/\" v103) "/\" ((v101 "/\" v103) "\/" v100))
A126:
for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" ((v1 "/\" v2) "\/" v0))) "/\" (v0 "\/" ((v1 "/\" v2) "\/" (v1 "/\" (v2 "/\" v0)))) = v0 "\/" ((v1 "/\" v2) "/\" ((v1 "/\" v2) "\/" v0))
A128:
for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" ((v1 "/\" v2) "\/" v0))) "/\" (v0 "\/" (v1 "/\" v2)) = v0 "\/" ((v1 "/\" v2) "/\" ((v1 "/\" v2) "\/" v0))
A130:
for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" (v1 "/\" ((v1 "/\" v2) "\/" v0))) = v0 "\/" ((v1 "/\" v2) "/\" ((v1 "/\" v2) "\/" v0))
A132:
for v0, v2, v1 being Element of L holds v0 "\/" ((v1 "/\" v2) "/\" (v1 "\/" v0)) = v0 "\/" ((v1 "/\" v2) "/\" ((v1 "/\" v2) "\/" v0))
A134:
for v2, v0, v1 being Element of L holds v0 "\/" (v1 "/\" (v2 "/\" (v1 "\/" v0))) = v0 "\/" ((v1 "/\" v2) "/\" ((v1 "/\" v2) "\/" v0))
A136:
for v2, v0, v1 being Element of L holds v0 "\/" (v1 "/\" (v2 "/\" (v1 "\/" v0))) = v0 "\/" ((v1 "/\" v2) "\/" ((v1 "/\" v2) "/\" v0))
A138:
for v2, v0, v1 being Element of L holds v0 "\/" (v1 "/\" (v2 "/\" (v1 "\/" v0))) = v0 "\/" ((v1 "/\" v2) "\/" (v1 "/\" (v2 "/\" v0)))
A140:
for v2, v0, v1 being Element of L holds v0 "\/" (v1 "/\" (v2 "/\" (v1 "\/" v0))) = v0 "\/" (v1 "/\" v2)
A143:
for v101, v2, v102 being Element of L holds (v102 "/\" v2) "\/" ((v101 "\/" (v102 "/\" v2)) "/\" v102) = (v102 "/\" v2) "\/" (v102 "/\" (v101 "/\" (v102 "\/" v2)))
A146:
for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" (v2 "\/" (v0 "/\" v1))) = (v0 "/\" v1) "\/" (v0 "/\" (v2 "/\" (v0 "\/" v1)))
A148:
for v2, v1, v0 being Element of L holds v0 "/\" (v2 "\/" (v0 "/\" v1)) = (v0 "/\" v1) "\/" (v0 "/\" (v2 "/\" (v0 "\/" v1)))
A154:
for v102, v2, v101 being Element of L holds (v101 "/\" v2) "\/" (v101 "/\" (v101 "/\" (v102 "/\" (v101 "\/" v2)))) = (v101 "/\" v2) "\/" (v101 "/\" v102)
A157:
for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" (v2 "/\" (v0 "\/" v1))) = (v0 "/\" v1) "\/" (v0 "/\" v2)
A159:
for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" v2) = v0 "/\" (v2 "\/" (v0 "/\" v1))
let v1, v2, v3 be Element of L; (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3))
v1 "/\" (v2 "\/" (v1 "/\" v3)) = (v1 "/\" v3) "\/" (v1 "/\" v2)
by A159;
hence
(v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3))
by A8; verum