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 "/\" (v0 "\/" v1)) = (v0 "\/" v1) "/\" (v2 "\/" (v0 "/\" v1)) ) implies for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) )
assume A1:
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 "/\" (v0 "\/" v1)) = (v0 "\/" v1) "/\" (v2 "\/" (v0 "/\" v1)) or for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) )
assume A2:
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 "/\" (v0 "\/" v1)) = (v0 "\/" v1) "/\" (v2 "\/" (v0 "/\" v1)) or for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) )
assume A3:
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 "/\" (v0 "\/" v1)) = (v0 "\/" v1) "/\" (v2 "\/" (v0 "/\" v1)) or for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) )
assume A4:
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 "/\" (v0 "\/" v1)) = (v0 "\/" v1) "/\" (v2 "\/" (v0 "/\" v1)) or for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) )
assume A5:
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 "/\" (v0 "\/" v1)) = (v0 "\/" v1) "/\" (v2 "\/" (v0 "/\" v1)) or for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) )
assume A6:
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 "/\" (v0 "\/" v1)) = (v0 "\/" v1) "/\" (v2 "\/" (v0 "/\" v1)) or for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) )
assume A7:
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 "/\" (v0 "\/" v1)) = (v0 "\/" v1) "/\" (v2 "\/" (v0 "/\" v1)) or for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) )
assume A8:
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 "/\" (v0 "\/" v1)) = (v0 "\/" v1) "/\" (v2 "\/" (v0 "/\" v1)) or for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) )
A10:
for v0, v2, v1 being Element of L holds (v0 "\/" v1) "/\" (v0 "\/" (v1 "/\" v2)) = v0 "\/" (v1 "/\" v2)
assume A11:
for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" (v0 "\/" v1)) = (v0 "\/" v1) "/\" (v2 "\/" (v0 "/\" v1))
; for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3))
A14:
for v0, v2, v1 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" (v1 "\/" v2)) = v0 "/\" (v1 "\/" v2)
A17:
for v102, v101 being Element of L holds v101 "/\" v102 = v101 "/\" (v101 "/\" v102)
A22:
for v102, v100 being Element of L holds (v100 "/\" v102) "/\" v102 = v100 "/\" v102
A25:
for v1, v0 being Element of L holds v1 "/\" (v0 "/\" v1) = v0 "/\" v1
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, v101 being Element of L holds v101 "\/" v102 = v101 "\/" (v101 "\/" v102)
A39:
for v102, v100 being Element of L holds (v100 "\/" v102) "\/" v102 = v100 "\/" v102
A42:
for v1, v0 being Element of L holds v1 "\/" (v0 "\/" v1) = v0 "\/" v1
A45:
for v2, v0, v1 being Element of L holds (v1 "\/" v0) "\/" v2 = v0 "\/" (v1 "\/" v2)
A48:
for v0, v2, v1 being Element of L holds v0 "\/" (v1 "\/" v2) = v1 "\/" (v0 "\/" v2)
A51:
for v102, v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" v102 = (v0 "\/" v1) "/\" ((v0 "\/" (v1 "/\" v2)) "/\" v102)
A55:
for v0, v2, v1 being Element of L holds (v1 "\/" v0) "/\" (v0 "\/" (v1 "/\" v2)) = v0 "\/" (v1 "/\" v2)
A59:
for v101, v102 being Element of L holds v101 "\/" (v102 "/\" (v101 "\/" v101)) = (v101 "\/" v101) "/\" (v102 "\/" (v101 "/\" v101))
A62:
for v0, v1 being Element of L holds v0 "\/" (v1 "/\" v0) = (v0 "\/" v0) "/\" (v1 "\/" (v0 "/\" v0))
A64:
for v0, v1 being Element of L holds v0 "\/" (v1 "/\" v0) = v0 "/\" (v1 "\/" (v0 "/\" v0))
A66:
for v0, v1 being Element of L holds v0 "\/" (v1 "/\" v0) = v0 "/\" (v1 "\/" v0)
A69:
for v0, v1, v101, v100 being Element of L holds (v100 "/\" v101) "\/" (v0 "/\" (v1 "/\" (v100 "\/" v101))) = (v100 "\/" v101) "/\" ((v0 "/\" v1) "\/" (v100 "/\" v101))
A72:
for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" (v0 "\/" v1)) = (v0 "\/" v1) "/\" ((v0 "/\" v1) "\/" v2)
A74:
for v0, v2, v1 being Element of L holds (v1 "/\" v0) "\/" (v0 "/\" (v1 "\/" v2)) = v0 "/\" (v1 "\/" v2)
A77:
for v0, v1, v2 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" (v2 "\/" v1)) = v0 "/\" (v1 "\/" v2)
A80:
for v101, v2, v1 being Element of L holds ((v101 "/\" v1) "\/" v101) "/\" (v101 "/\" (v1 "\/" v2)) = (v101 "/\" v1) "\/" (v101 "/\" (v1 "\/" v2))
A83:
for v0, v2, v1 being Element of L holds (v0 "\/" (v0 "/\" v1)) "/\" (v0 "/\" (v1 "\/" v2)) = (v0 "/\" v1) "\/" (v0 "/\" (v1 "\/" v2))
A85:
for v2, v1, v0 being Element of L holds v0 "/\" ((v0 "\/" (v0 "/\" v1)) "/\" (v1 "\/" v2)) = (v0 "/\" v1) "\/" (v0 "/\" (v1 "\/" v2))
A87:
for v2, v1, v0 being Element of L holds v0 "/\" ((v0 "\/" (v0 "/\" v1)) "/\" (v1 "\/" v2)) = v0 "/\" (v1 "\/" v2)
A90:
for v102, v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "\/" ((v0 "\/" v1) "/\" ((v0 "\/" (v1 "/\" v2)) "\/" v102)) = (v0 "\/" v1) "/\" ((v0 "\/" (v1 "/\" v2)) "\/" v102)
A93:
for v0, v3, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "\/" ((v0 "\/" v1) "/\" (v0 "\/" ((v1 "/\" v2) "\/" v3))) = (v0 "\/" v1) "/\" ((v0 "\/" (v1 "/\" v2)) "\/" v3)
A95:
for v0, v3, v2, v1 being Element of L holds v0 "\/" ((v1 "/\" v2) "\/" ((v0 "\/" v1) "/\" (v0 "\/" ((v1 "/\" v2) "\/" v3)))) = (v0 "\/" v1) "/\" ((v0 "\/" (v1 "/\" v2)) "\/" v3)
A97:
for v0, v3, v2, v1 being Element of L holds v0 "\/" ((v1 "/\" v2) "\/" ((v0 "\/" v1) "/\" (v0 "\/" ((v1 "/\" v2) "\/" v3)))) = (v0 "\/" v1) "/\" (v0 "\/" ((v1 "/\" v2) "\/" v3))
A100:
for v102, v1, v100 being Element of L holds (v100 "/\" v1) "\/" (v100 "/\" ((v100 "/\" v1) "\/" v102)) = v100 "/\" ((v100 "/\" v1) "\/" v102)
A104:
for v0, v100, v1 being Element of L holds v100 "\/" (v0 "\/" (v1 "\/" v100)) = (v0 "\/" v1) "\/" v100
A107:
for v1, v0, v2 being Element of L holds v0 "\/" (v1 "\/" (v2 "\/" v0)) = v1 "\/" (v2 "\/" v0)
A109:
for v1, v0 being Element of L holds v0 "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v0)
A112:
for v102, v100, v1 being Element of L holds (v100 "/\" (v1 "\/" v100)) "\/" v102 = v100 "\/" ((v1 "/\" v100) "\/" v102)
A115:
for v0, v1 being Element of L holds v0 "\/" (v1 "/\" v0) = v0 "/\" (v0 "\/" v1)
A117:
for v1, v0 being Element of L holds v0 "\/" (v0 "/\" v1) = v0 "/\" (v0 "\/" v1)
A119:
for v2, v1, v0 being Element of L holds v0 "/\" ((v0 "/\" (v0 "\/" v1)) "/\" (v1 "\/" v2)) = v0 "/\" (v1 "\/" v2)
A121:
for v2, v1, v0 being Element of L holds v0 "/\" (v0 "/\" ((v0 "\/" v1) "/\" (v1 "\/" v2))) = v0 "/\" (v1 "\/" v2)
A123:
for v2, v1, v0 being Element of L holds v0 "/\" ((v0 "\/" v1) "/\" (v1 "\/" v2)) = v0 "/\" (v1 "\/" v2)
A126:
for v102, v1, v100 being Element of L holds (v100 "/\" (v100 "\/" v1)) "\/" v102 = v100 "\/" ((v1 "/\" v100) "\/" v102)
A130:
for v101, v102 being Element of L holds (v102 "\/" v101) "/\" (v101 "\/" v102) = v101 "\/" (v102 "/\" v102)
A133:
for v1, v0 being Element of L holds (v0 "\/" v1) "/\" (v1 "\/" v0) = v1 "\/" v0
A136:
for v101, v100, v1 being Element of L holds (v100 "\/" v101) "/\" (v101 "\/" (v1 "/\" v100)) = v101 "\/" (v100 "/\" (v1 "/\" v100))
A139:
for v1, v0, v2 being Element of L holds (v0 "\/" v1) "/\" (v1 "\/" (v2 "/\" v0)) = v1 "\/" (v2 "/\" v0)
A142:
for v102, v1, v100 being Element of L holds (v100 "/\" (v100 "\/" v1)) "/\" ((v100 "/\" v1) "\/" (v100 "/\" v102)) = (v100 "/\" v1) "\/" (v100 "/\" v102)
A145:
for v2, v1, v0 being Element of L holds v0 "/\" ((v0 "\/" v1) "/\" ((v0 "/\" v1) "\/" (v0 "/\" v2))) = (v0 "/\" v1) "\/" (v0 "/\" v2)
A148:
for v100, v102, v101 being Element of L holds (v100 "\/" v101) "/\" ((v101 "/\" v102) "\/" v100) = (v100 "\/" (v101 "/\" v102)) "/\" ((v101 "/\" v102) "\/" v100)
A151:
for v0, v2, v1 being Element of L holds (v0 "\/" v1) "/\" ((v1 "/\" v2) "\/" v0) = (v1 "/\" v2) "\/" v0
A154:
for v101, v102 being Element of L holds (v102 "/\" v101) "\/" (v101 "/\" v102) = v101 "/\" (v102 "\/" v102)
A157:
for v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v1 "/\" v0) = v1 "/\" v0
A159:
for v1, v0, v2 being Element of L holds (v0 "/\" v1) "\/" (v1 "/\" (v2 "\/" v0)) = v1 "/\" (v0 "\/" v2)
A162:
for v102, v0, v1 being Element of L holds (v1 "/\" v0) "\/" v102 = (v0 "/\" v1) "\/" ((v1 "/\" v0) "\/" v102)
A168:
for v101, v2, v1 being Element of L holds ((v101 "\/" v1) "/\" v101) "\/" ((v101 "\/" v1) "/\" ((v1 "/\" v2) "\/" v101)) = v101 "\/" (v1 "/\" v2)
A171:
for v0, v2, v1 being Element of L holds (v0 "/\" (v0 "\/" v1)) "\/" ((v0 "\/" v1) "/\" ((v1 "/\" v2) "\/" v0)) = v0 "\/" (v1 "/\" v2)
A173:
for v0, v2, v1 being Element of L holds (v0 "/\" (v0 "\/" v1)) "\/" ((v1 "/\" v2) "\/" v0) = v0 "\/" (v1 "/\" v2)
A175:
for v0, v2, v1 being Element of L holds v0 "\/" ((v1 "/\" v0) "\/" ((v1 "/\" v2) "\/" v0)) = v0 "\/" (v1 "/\" v2)
A177:
for v0, v2, v1 being Element of L holds (v1 "/\" v0) "\/" ((v1 "/\" v2) "\/" v0) = v0 "\/" (v1 "/\" v2)
A180:
for v2, v3, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" (v3 "/\" (v0 "\/" v1))) = (v0 "\/" v1) "/\" ((v0 "/\" v1) "\/" (v2 "/\" v3))
A183:
for v102, v1, v100 being Element of L holds v100 "/\" ((v100 "/\" (v100 "\/" v1)) "/\" ((v100 "/\" v1) "\/" v102)) = v100 "/\" ((v100 "/\" v1) "\/" v102)
A186:
for v2, v1, v0 being Element of L holds v0 "/\" (v0 "/\" ((v0 "\/" v1) "/\" ((v0 "/\" v1) "\/" v2))) = v0 "/\" ((v0 "/\" v1) "\/" v2)
A188:
for v2, v1, v0 being Element of L holds v0 "/\" ((v0 "\/" v1) "/\" ((v0 "/\" v1) "\/" v2)) = v0 "/\" ((v0 "/\" v1) "\/" v2)
A190:
for v2, v1, v0 being Element of L holds v0 "/\" ((v0 "/\" v1) "\/" (v0 "/\" v2)) = (v0 "/\" v1) "\/" (v0 "/\" v2)
A193:
for v102, v1, v100 being Element of L holds (v100 "/\" v1) "\/" (v102 "/\" (v100 "\/" (v100 "/\" v1))) = (v100 "\/" (v100 "/\" v1)) "/\" ((v100 "/\" (v100 "/\" v1)) "\/" v102)
A196:
for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" (v0 "/\" (v0 "\/" v1))) = (v0 "\/" (v0 "/\" v1)) "/\" ((v0 "/\" (v0 "/\" v1)) "\/" v2)
A198:
for v2, v1, v0 being Element of L holds (v0 "\/" v1) "/\" ((v0 "/\" v1) "\/" (v2 "/\" v0)) = (v0 "\/" (v0 "/\" v1)) "/\" ((v0 "/\" (v0 "/\" v1)) "\/" v2)
A200:
for v2, v1, v0 being Element of L holds (v0 "\/" v1) "/\" ((v0 "/\" v1) "\/" (v2 "/\" v0)) = (v0 "/\" (v0 "\/" v1)) "/\" ((v0 "/\" (v0 "/\" v1)) "\/" v2)
A202:
for v2, v1, v0 being Element of L holds (v0 "\/" v1) "/\" ((v0 "/\" v1) "\/" (v2 "/\" v0)) = (v0 "/\" (v0 "\/" v1)) "/\" ((v0 "/\" v1) "\/" v2)
A204:
for v2, v1, v0 being Element of L holds (v0 "\/" v1) "/\" ((v0 "/\" v1) "\/" (v2 "/\" v0)) = v0 "/\" ((v0 "\/" v1) "/\" ((v0 "/\" v1) "\/" v2))
A206:
for v2, v1, v0 being Element of L holds (v0 "\/" v1) "/\" ((v0 "/\" v1) "\/" (v2 "/\" v0)) = v0 "/\" ((v0 "/\" v1) "\/" v2)
A209:
for v102, v1, v100 being Element of L holds (v100 "/\" (v100 "\/" v1)) "/\" ((v100 "/\" v1) "\/" (v102 "/\" v100)) = (v100 "/\" v1) "\/" (v102 "/\" v100)
A212:
for v2, v1, v0 being Element of L holds v0 "/\" ((v0 "\/" v1) "/\" ((v0 "/\" v1) "\/" (v2 "/\" v0))) = (v0 "/\" v1) "\/" (v2 "/\" v0)
A214:
for v2, v1, v0 being Element of L holds v0 "/\" (v0 "/\" ((v0 "/\" v1) "\/" v2)) = (v0 "/\" v1) "\/" (v2 "/\" v0)
A216:
for v2, v1, v0 being Element of L holds v0 "/\" ((v0 "/\" v1) "\/" v2) = (v0 "/\" v1) "\/" (v2 "/\" v0)
A220:
for v100, v0, v2 being Element of L holds (v100 "/\" (v0 "\/" v100)) "\/" (v100 "\/" (v2 "/\" v0)) = (v0 "\/" v100) "/\" (v100 "\/" (v2 "/\" v0))
A223:
for v2, v0, v1 being Element of L holds v0 "\/" ((v0 "/\" (v1 "\/" v0)) "\/" (v2 "/\" v1)) = (v1 "\/" v0) "/\" (v0 "\/" (v2 "/\" v1))
A225:
for v2, v0, v1 being Element of L holds v0 "\/" (v0 "\/" ((v1 "/\" v0) "\/" (v2 "/\" v1))) = (v1 "\/" v0) "/\" (v0 "\/" (v2 "/\" v1))
A227:
for v2, v0, v1 being Element of L holds v0 "\/" (v0 "\/" (v1 "/\" ((v1 "/\" v0) "\/" v2))) = (v1 "\/" v0) "/\" (v0 "\/" (v2 "/\" v1))
A229:
for v2, v0, v1 being Element of L holds v0 "\/" (v1 "/\" ((v1 "/\" v0) "\/" v2)) = (v1 "\/" v0) "/\" (v0 "\/" (v2 "/\" v1))
A231:
for v2, v0, v1 being Element of L holds v0 "\/" (v1 "/\" ((v1 "/\" v0) "\/" v2)) = v0 "\/" (v2 "/\" v1)
A234:
for v1, v102, v100 being Element of L holds (v1 "/\" v100) "\/" ((v100 "/\" v102) "\/" (v1 "/\" v100)) = (v1 "/\" v100) "\/" (v100 "/\" v102)
A237:
for v0, v2, v1 being Element of L holds (v0 "/\" v1) "\/" (v1 "/\" ((v1 "/\" v2) "\/" v0)) = (v0 "/\" v1) "\/" (v1 "/\" v2)
A239:
for v0, v2, v1 being Element of L holds v1 "/\" (v0 "\/" (v1 "/\" v2)) = (v0 "/\" v1) "\/" (v1 "/\" v2)
A245:
for v103, v102, v101 being Element of L holds (v102 "/\" v101) "\/" ((v101 "/\" v102) "\/" (((v102 "/\" v101) "\/" v101) "/\" ((v101 "/\" v102) "\/" v103))) = ((v102 "/\" v101) "\/" v101) "/\" ((v102 "/\" v101) "\/" ((v101 "/\" v102) "\/" v103))
A248:
for v2, v0, v1 being Element of L holds (v0 "/\" v1) "\/" ((v1 "/\" v0) "\/" ((v1 "\/" (v0 "/\" v1)) "/\" ((v1 "/\" v0) "\/" v2))) = ((v0 "/\" v1) "\/" v1) "/\" ((v0 "/\" v1) "\/" ((v1 "/\" v0) "\/" v2))
A250:
for v2, v0, v1 being Element of L holds (v0 "/\" v1) "\/" ((v1 "/\" v0) "\/" ((v1 "/\" (v1 "\/" v0)) "/\" ((v1 "/\" v0) "\/" v2))) = ((v0 "/\" v1) "\/" v1) "/\" ((v0 "/\" v1) "\/" ((v1 "/\" v0) "\/" v2))
A252:
for v2, v0, v1 being Element of L holds (v0 "/\" v1) "\/" ((v1 "/\" v0) "\/" (v1 "/\" ((v1 "\/" v0) "/\" ((v1 "/\" v0) "\/" v2)))) = ((v0 "/\" v1) "\/" v1) "/\" ((v0 "/\" v1) "\/" ((v1 "/\" v0) "\/" v2))
A254:
for v2, v0, v1 being Element of L holds (v0 "/\" v1) "\/" ((v1 "/\" v0) "\/" (v1 "/\" ((v1 "/\" v0) "\/" v2))) = ((v0 "/\" v1) "\/" v1) "/\" ((v0 "/\" v1) "\/" ((v1 "/\" v0) "\/" v2))
A256:
for v2, v0, v1 being Element of L holds (v0 "/\" v1) "\/" (v1 "/\" ((v1 "/\" v0) "\/" v2)) = ((v0 "/\" v1) "\/" v1) "/\" ((v0 "/\" v1) "\/" ((v1 "/\" v0) "\/" v2))
A258:
for v2, v0, v1 being Element of L holds v1 "/\" (v0 "\/" (v1 "/\" ((v1 "/\" v0) "\/" v2))) = ((v0 "/\" v1) "\/" v1) "/\" ((v0 "/\" v1) "\/" ((v1 "/\" v0) "\/" v2))
A261:
for v1, v0, v2 being Element of L holds v0 "/\" (v1 "\/" (v2 "/\" v0)) = ((v1 "/\" v0) "\/" v0) "/\" ((v1 "/\" v0) "\/" ((v0 "/\" v1) "\/" v2))
A263:
for v1, v0, v2 being Element of L holds v0 "/\" (v1 "\/" (v2 "/\" v0)) = (v0 "\/" (v1 "/\" v0)) "/\" ((v1 "/\" v0) "\/" ((v0 "/\" v1) "\/" v2))
A265:
for v1, v0, v2 being Element of L holds v0 "/\" (v1 "\/" (v2 "/\" v0)) = (v0 "/\" (v0 "\/" v1)) "/\" ((v1 "/\" v0) "\/" ((v0 "/\" v1) "\/" v2))
A267:
for v1, v0, v2 being Element of L holds v0 "/\" (v1 "\/" (v2 "/\" v0)) = (v0 "/\" (v0 "\/" v1)) "/\" ((v0 "/\" v1) "\/" v2)
A269:
for v1, v0, v2 being Element of L holds v0 "/\" (v1 "\/" (v2 "/\" v0)) = v0 "/\" ((v0 "\/" v1) "/\" ((v0 "/\" v1) "\/" v2))
A271:
for v1, v0, v2 being Element of L holds v0 "/\" (v1 "\/" (v2 "/\" v0)) = v0 "/\" ((v0 "/\" v1) "\/" v2)
A274:
for v1, v2, v0 being Element of L holds v0 "/\" (v1 "\/" ((v0 "/\" v2) "/\" v0)) = (v0 "/\" v1) "\/" (v0 "/\" v2)
A276:
for v1, v2, v0 being Element of L holds v0 "/\" (v1 "\/" (v0 "/\" (v0 "/\" v2))) = (v0 "/\" v1) "\/" (v0 "/\" v2)
for v1, v2, v0 being Element of L holds v0 "/\" (v1 "\/" (v0 "/\" v2)) = (v0 "/\" v1) "\/" (v0 "/\" v2)
hence
for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3))
; verum