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 v1, v2, v0 being Element of L holds v0 "/\" (v1 "\/" (v0 "/\" v2)) = v0 "/\" (v1 "\/" v2) ) implies for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" v3) )
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 v1, v2, v0 being Element of L st not v0 "/\" (v1 "\/" (v0 "/\" v2)) = v0 "/\" (v1 "\/" v2) or for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" v3) )
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 v1, v2, v0 being Element of L st not v0 "/\" (v1 "\/" (v0 "/\" v2)) = v0 "/\" (v1 "\/" v2) or for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" v3) )
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 v1, v2, v0 being Element of L st not v0 "/\" (v1 "\/" (v0 "/\" v2)) = v0 "/\" (v1 "\/" v2) or for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" v3) )
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 v1, v2, v0 being Element of L st not v0 "/\" (v1 "\/" (v0 "/\" v2)) = v0 "/\" (v1 "\/" v2) or for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" v3) )
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 v1, v2, v0 being Element of L st not v0 "/\" (v1 "\/" (v0 "/\" v2)) = v0 "/\" (v1 "\/" v2) or for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" v3) )
assume A6:
for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2)
; ( ex v1, v2, v0 being Element of L st not v0 "/\" (v1 "\/" (v0 "/\" v2)) = v0 "/\" (v1 "\/" v2) or for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" v3) )
A8:
for v0, v2, v1 being Element of L holds (v0 "\/" v1) "/\" (v0 "\/" (v1 "/\" v2)) = v0 "\/" (v1 "/\" v2)
assume A9:
for v1, v2, v0 being Element of L holds v0 "/\" (v1 "\/" (v0 "/\" v2)) = v0 "/\" (v1 "\/" v2)
; for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" v3)
A12:
for v0, v2, v1 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" (v1 "\/" v2)) = v0 "/\" (v1 "\/" v2)
A15:
for v102, v100 being Element of L holds (v100 "\/" v102) "\/" v102 = v100 "\/" v102
A18:
for v1, v0 being Element of L holds v1 "\/" (v0 "\/" v1) = v0 "\/" v1
A21:
for v2, v0, v1 being Element of L holds (v1 "\/" v0) "\/" v2 = v0 "\/" (v1 "\/" v2)
A24:
for v0, v2, v1 being Element of L holds v0 "\/" (v1 "\/" v2) = v1 "\/" (v0 "\/" v2)
A27:
for v102, v101 being Element of L holds v101 "/\" (v101 "\/" (v101 "/\" v102)) = v101 "\/" (v101 "/\" v102)
A30:
for v1, v0 being Element of L holds v0 "/\" (v0 "\/" v1) = v0 "\/" (v0 "/\" v1)
A33:
for v1, v0, v2 being Element of L holds v0 "/\" (v1 "\/" (v2 "/\" v0)) = v0 "/\" (v1 "\/" v2)
A35:
for v0, v1, v2 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" (v2 "\/" v1)) = v0 "/\" (v1 "\/" v2)
A37:
for v0, v1 being Element of L holds v0 "\/" (v1 "/\" v0) = v0 "/\" (v0 "\/" v1)
A40:
for v1, v2, v101 being Element of L holds (v1 "\/" (v101 "/\" v2)) "\/" (v101 "/\" (v1 "\/" v2)) = (v1 "\/" (v101 "/\" v2)) "/\" ((v1 "\/" (v101 "/\" v2)) "\/" v101)
A43:
for v1, v2, v0 being Element of L holds (v1 "/\" (v0 "\/" v2)) "\/" (v0 "\/" (v1 "/\" v2)) = (v0 "\/" (v1 "/\" v2)) "/\" ((v0 "\/" (v1 "/\" v2)) "\/" v1)
A46:
for v0, v2, v1 being Element of L holds v1 "\/" ((v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v2)) = (v1 "\/" (v0 "/\" v2)) "/\" ((v1 "\/" (v0 "/\" v2)) "\/" v0)
A49:
for v1, v2, v0 being Element of L holds v0 "\/" ((v1 "/\" v2) "\/" (v1 "/\" (v0 "\/" v2))) = (v0 "\/" (v1 "/\" v2)) "/\" ((v0 "\/" (v1 "/\" v2)) "\/" v1)
A51:
for v1, v0, v2 being Element of L holds v0 "\/" (v1 "/\" (v2 "\/" v0)) = (v0 "\/" (v1 "/\" v2)) "/\" ((v0 "\/" (v1 "/\" v2)) "\/" v1)
A53:
for v1, v0, v2 being Element of L holds v0 "\/" (v1 "/\" (v2 "\/" v0)) = (v0 "\/" (v1 "/\" v2)) "/\" (v1 "\/" (v0 "\/" (v1 "/\" v2)))
A56:
for v101, v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v101 "\/" (v0 "\/" (v1 "/\" v2))) = (v0 "\/" (v1 "/\" v2)) "/\" (v101 "\/" (v0 "\/" v1))
A59:
for v1, v0, v2 being Element of L holds v0 "\/" (v1 "/\" (v2 "\/" v0)) = (v0 "\/" (v1 "/\" v2)) "/\" (v1 "\/" (v0 "\/" v1))
A61:
for v1, v0, v2 being Element of L holds v0 "\/" (v1 "/\" (v2 "\/" v0)) = (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1)
A63:
for v1, v0, v2 being Element of L holds v0 "\/" (v1 "/\" (v2 "\/" v0)) = (v0 "\/" v1) "/\" (v0 "\/" (v1 "/\" v2))
A65:
for v1, v0, v2 being Element of L holds v0 "\/" (v1 "/\" (v2 "\/" v0)) = v0 "\/" (v1 "/\" v2)
A68:
for v101, v2, v102 being Element of L holds (v101 "/\" v2) "\/" (v101 "/\" (v102 "\/" v2)) = (v101 "/\" v2) "\/" (v101 "/\" v102)
for v0, v2, v1 being Element of L holds v0 "/\" (v1 "\/" v2) = (v0 "/\" v1) "\/" (v0 "/\" v2)
hence
for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" v3)
; verum