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 "/\" v0) = (((v0 "\/" v1) "/\" v2) "\/" v1) "/\" (v2 "\/" v0) ) implies for v1, v2, v3 being Element of L holds v1 "\/" (v2 "/\" 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 "/\" v0) = (((v0 "\/" v1) "/\" v2) "\/" v1) "/\" (v2 "\/" v0) or for v1, v2, v3 being Element of L holds v1 "\/" (v2 "/\" 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 "/\" v0) = (((v0 "\/" v1) "/\" v2) "\/" v1) "/\" (v2 "\/" v0) or for v1, v2, v3 being Element of L holds v1 "\/" (v2 "/\" 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 "/\" v0) = (((v0 "\/" v1) "/\" v2) "\/" v1) "/\" (v2 "\/" v0) or for v1, v2, v3 being Element of L holds v1 "\/" (v2 "/\" 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 "/\" v0) = (((v0 "\/" v1) "/\" v2) "\/" v1) "/\" (v2 "\/" v0) or for v1, v2, v3 being Element of L holds v1 "\/" (v2 "/\" 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 "/\" v0) = (((v0 "\/" v1) "/\" v2) "\/" v1) "/\" (v2 "\/" v0) or for v1, v2, v3 being Element of L holds v1 "\/" (v2 "/\" 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 "/\" v0) = (((v0 "\/" v1) "/\" v2) "\/" v1) "/\" (v2 "\/" v0) or for v1, v2, v3 being Element of L holds v1 "\/" (v2 "/\" 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 "/\" v0) = (((v0 "\/" v1) "/\" v2) "\/" v1) "/\" (v2 "\/" v0) or for v1, v2, v3 being Element of L holds v1 "\/" (v2 "/\" 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 "/\" v0) = (((v0 "\/" v1) "/\" v2) "\/" v1) "/\" (v2 "\/" v0) or for v1, v2, v3 being Element of L holds v1 "\/" (v2 "/\" 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 "/\" v0) = (((v0 "\/" v1) "/\" v2) "\/" v1) "/\" (v2 "\/" v0)
; for v1, v2, v3 being Element of L holds v1 "\/" (v2 "/\" v3) = (v1 "\/" v2) "/\" (v1 "\/" v3)
A14:
for v2, v1, v0 being Element of L holds (v1 "/\" ((v0 "/\" v1) "\/" v2)) "\/" (v2 "/\" v0) = (((v0 "\/" v1) "/\" v2) "\/" v1) "/\" (v2 "\/" v0)
A17:
for v2, v0, v1 being Element of L holds (v2 "/\" v1) "\/" (v0 "/\" ((v1 "/\" v0) "\/" v2)) = (((v1 "\/" v0) "/\" v2) "\/" v0) "/\" (v2 "\/" v1)
A20:
for v0, v2, v1 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" ((v1 "/\" v2) "\/" v0)) = (v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v0 "\/" v1)
A23:
for v0, v2, v1 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" (v1 "\/" v2)) = v0 "/\" (v1 "\/" v2)
A26:
for v102, v101 being Element of L holds v101 "/\" v102 = v101 "/\" (v101 "/\" v102)
A31:
for v102, v100 being Element of L holds (v100 "/\" v102) "/\" v102 = v100 "/\" v102
A34:
for v1, v0 being Element of L holds v1 "/\" (v0 "/\" v1) = v0 "/\" v1
A37:
for v2, v0, v1 being Element of L holds (v1 "/\" v0) "/\" v2 = v0 "/\" (v1 "/\" v2)
A40:
for v0, v2, v1 being Element of L holds v0 "/\" (v1 "/\" v2) = v1 "/\" (v0 "/\" v2)
A43:
for v102, v101 being Element of L holds v101 "\/" v102 = v101 "\/" (v101 "\/" v102)
A48:
for v102, v100 being Element of L holds (v100 "\/" v102) "\/" v102 = v100 "\/" v102
A51:
for v1, v0 being Element of L holds v1 "\/" (v0 "\/" v1) = v0 "\/" v1
A54:
for v2, v0, v1 being Element of L holds (v1 "\/" v0) "\/" v2 = v0 "\/" (v1 "\/" v2)
A57:
for v0, v2, v1 being Element of L holds v0 "\/" (v1 "\/" v2) = v1 "\/" (v0 "\/" v2)
A60:
for v102, v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" v102 = (v0 "\/" v1) "/\" ((v0 "\/" (v1 "/\" v2)) "/\" v102)
A65:
for v100, v0, v102, v1 being Element of L holds (v100 "\/" (v0 "/\" v1)) "/\" (v100 "\/" (v0 "/\" (v1 "/\" v102))) = v100 "\/" ((v0 "/\" v1) "/\" v102)
A68:
for v0, v1, v3, v2 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" (v1 "/\" (v2 "/\" v3))) = v0 "\/" (v1 "/\" (v2 "/\" v3))
A71:
for v102, v101 being Element of L holds v101 "/\" (v101 "\/" (v101 "/\" v102)) = v101 "\/" (v101 "/\" v102)
A75:
for v102, v101 being Element of L holds ((v101 "/\" v102) "\/" v101) "/\" (v101 "/\" v102) = (v101 "/\" v102) "\/" (v101 "/\" v102)
A78:
for v1, v0 being Element of L holds (v0 "\/" (v0 "/\" v1)) "/\" (v0 "/\" v1) = (v0 "/\" v1) "\/" (v0 "/\" v1)
A80:
for v1, v0 being Element of L holds (v0 "/\" v1) "/\" (v0 "\/" (v0 "/\" v1)) = (v0 "/\" v1) "\/" (v0 "/\" v1)
A82:
for v1, v0 being Element of L holds v0 "/\" (v1 "/\" (v0 "\/" (v0 "/\" v1))) = (v0 "/\" v1) "\/" (v0 "/\" v1)
A84:
for v1, v0 being Element of L holds v0 "/\" (v1 "/\" (v0 "\/" (v0 "/\" v1))) = v0 "/\" v1
A86:
for v0, v2, v1 being Element of L holds (v1 "\/" v0) "/\" (v0 "\/" (v1 "/\" v2)) = v0 "\/" (v1 "/\" v2)
A90:
for v102, v101 being Element of L holds v101 "\/" (v102 "/\" ((v101 "/\" v102) "\/" v101)) = (v102 "\/" ((v101 "\/" v102) "/\" v101)) "/\" (v101 "\/" v101)
A93:
for v1, v0 being Element of L holds v0 "\/" (v1 "/\" (v0 "\/" (v0 "/\" v1))) = (v1 "\/" ((v0 "\/" v1) "/\" v0)) "/\" (v0 "\/" v0)
A95:
for v1, v0 being Element of L holds v0 "\/" (v1 "/\" (v0 "\/" (v0 "/\" v1))) = (v1 "\/" (v0 "/\" (v0 "\/" v1))) "/\" (v0 "\/" v0)
A97:
for v1, v0 being Element of L holds v0 "\/" (v1 "/\" (v0 "\/" (v0 "/\" v1))) = (v1 "\/" (v0 "/\" (v0 "\/" v1))) "/\" v0
A99:
for v1, v0 being Element of L holds v0 "\/" (v1 "/\" (v0 "\/" (v0 "/\" v1))) = v0 "/\" (v1 "\/" (v0 "/\" (v0 "\/" v1)))
A101:
for v0, v2, v1 being Element of L holds (v1 "/\" v0) "\/" (v2 "/\" ((v1 "/\" v2) "\/" v0)) = (v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v0 "\/" v1)
A104:
for v0, v1, v2 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" ((v2 "/\" v1) "\/" v0)) = (v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v0 "\/" v1)
A107:
for v101, v1, v0 being Element of L holds ((v0 "/\" v1) "\/" v101) "/\" ((v101 "\/" ((v1 "\/" v101) "/\" v0)) "/\" (v0 "\/" v1)) = (v0 "/\" v1) "\/" (v101 "/\" ((v1 "/\" v101) "\/" v0))
A110:
for v2, v1, v0 being Element of L holds ((v0 "/\" v1) "\/" v2) "/\" ((v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v0 "\/" v1)) = (v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v0 "\/" v1)
A113:
for v102, v101 being Element of L holds v101 "\/" (v101 "/\" (v101 "\/" v102)) = v101 "/\" (v101 "\/" v102)
A117:
for v102, v101 being Element of L holds ((v101 "\/" v102) "/\" v101) "\/" (v101 "\/" v102) = (v101 "\/" v102) "/\" (v101 "\/" v102)
A120:
for v1, v0 being Element of L holds (v0 "/\" (v0 "\/" v1)) "\/" (v0 "\/" v1) = (v0 "\/" v1) "/\" (v0 "\/" v1)
A122:
for v1, v0 being Element of L holds (v0 "\/" v1) "\/" (v0 "/\" (v0 "\/" v1)) = (v0 "\/" v1) "/\" (v0 "\/" v1)
A124:
for v1, v0 being Element of L holds v0 "\/" (v1 "\/" (v0 "/\" (v0 "\/" v1))) = (v0 "\/" v1) "/\" (v0 "\/" v1)
A126:
for v1, v0 being Element of L holds v0 "\/" (v1 "\/" (v0 "/\" (v0 "\/" v1))) = v0 "\/" v1
A128:
for v0, v2, v1 being Element of L holds (v1 "/\" v0) "\/" (v0 "/\" (v1 "\/" v2)) = v0 "/\" (v1 "\/" v2)
A131:
for v0, v2, v1 being Element of L holds (v0 "/\" v1) "\/" ((v1 "\/" v2) "/\" v0) = v0 "/\" (v1 "\/" v2)
A133:
for v0, v1, v2 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" (v2 "\/" v1)) = v0 "/\" (v1 "\/" v2)
A136:
for v101, v2, v1 being Element of L holds ((v101 "/\" v1) "\/" v101) "/\" (v101 "/\" (v1 "\/" v2)) = (v101 "/\" v1) "\/" (v101 "/\" (v1 "\/" v2))
A139:
for v0, v2, v1 being Element of L holds (v0 "\/" (v0 "/\" v1)) "/\" (v0 "/\" (v1 "\/" v2)) = (v0 "/\" v1) "\/" (v0 "/\" (v1 "\/" v2))
A141:
for v2, v1, v0 being Element of L holds v0 "/\" ((v0 "\/" (v0 "/\" v1)) "/\" (v1 "\/" v2)) = (v0 "/\" v1) "\/" (v0 "/\" (v1 "\/" v2))
A143:
for v2, v1, v0 being Element of L holds v0 "/\" ((v0 "\/" (v0 "/\" v1)) "/\" (v1 "\/" v2)) = v0 "/\" (v1 "\/" v2)
A146:
for v101, v2, v1 being Element of L holds ((v101 "\/" v1) "/\" v101) "\/" (v101 "\/" (v1 "/\" v2)) = (v101 "\/" v1) "/\" (v101 "\/" (v1 "/\" v2))
A149:
for v0, v2, v1 being Element of L holds (v0 "/\" (v0 "\/" v1)) "\/" (v0 "\/" (v1 "/\" v2)) = (v0 "\/" v1) "/\" (v0 "\/" (v1 "/\" v2))
A151:
for v2, v1, v0 being Element of L holds v0 "\/" ((v0 "/\" (v0 "\/" v1)) "\/" (v1 "/\" v2)) = (v0 "\/" v1) "/\" (v0 "\/" (v1 "/\" v2))
A153:
for v2, v1, v0 being Element of L holds v0 "\/" ((v0 "/\" (v0 "\/" v1)) "\/" (v1 "/\" v2)) = v0 "\/" (v1 "/\" v2)
A156:
for v1, v101, v100 being Element of L holds (v100 "/\" v101) "/\" (v101 "/\" v1) = v100 "/\" (v101 "/\" v1)
A159:
for v2, v1, v0 being Element of L holds v1 "/\" ((v0 "/\" v1) "/\" v2) = v0 "/\" (v1 "/\" v2)
A162:
for v1, v2, v0 being Element of L holds v0 "/\" (v1 "/\" (v0 "/\" v2)) = v1 "/\" (v0 "/\" v2)
A165:
for v102, v1, v100 being Element of L holds (v100 "/\" v1) "\/" (v102 "/\" (((v100 "/\" v1) "/\" v102) "\/" v100)) = (v102 "\/" (((v100 "/\" v1) "\/" v102) "/\" v100)) "/\" (v100 "\/" (v100 "/\" v1))
A168:
for v0, v2, v1 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" ((v0 "/\" (v1 "/\" v2)) "\/" v0)) = (v2 "\/" (((v0 "/\" v1) "\/" v2) "/\" v0)) "/\" (v0 "\/" (v0 "/\" v1))
A170:
for v0, v2, v1 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" (v0 "\/" (v0 "/\" (v1 "/\" v2)))) = (v2 "\/" (((v0 "/\" v1) "\/" v2) "/\" v0)) "/\" (v0 "\/" (v0 "/\" v1))
A172:
for v0, v2, v1 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" (v0 "\/" (v0 "/\" (v1 "/\" v2)))) = (v2 "\/" (v0 "/\" ((v0 "/\" v1) "\/" v2))) "/\" (v0 "\/" (v0 "/\" v1))
A174:
for v0, v2, v1 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" (v0 "\/" (v0 "/\" (v1 "/\" v2)))) = (v0 "\/" (v0 "/\" v1)) "/\" (v2 "\/" (v0 "/\" ((v0 "/\" v1) "\/" v2)))
A177:
for v0, v100, v1 being Element of L holds v100 "/\" (v0 "/\" (v1 "/\" v100)) = (v0 "/\" v1) "/\" v100
A180:
for v1, v0, v2 being Element of L holds v0 "/\" (v1 "/\" (v2 "/\" v0)) = v1 "/\" (v2 "/\" v0)
A183:
for v100, v101, v1 being Element of L holds (v100 "\/" v101) "/\" (v100 "\/" (v1 "/\" v101)) = v100 "\/" (v101 "/\" (v1 "/\" v101))
A186:
for v0, v1, v2 being Element of L holds (v0 "\/" v1) "/\" (v0 "\/" (v2 "/\" v1)) = v0 "\/" (v2 "/\" v1)
A189:
for v1, v101, v100 being Element of L holds (v100 "\/" v101) "\/" (v101 "\/" v1) = v100 "\/" (v101 "\/" v1)
A192:
for v2, v1, v0 being Element of L holds v1 "\/" ((v0 "\/" v1) "\/" v2) = v0 "\/" (v1 "\/" v2)
A195:
for v1, v2, v0 being Element of L holds v0 "\/" (v1 "\/" (v0 "\/" v2)) = v1 "\/" (v0 "\/" v2)
A198:
for v102, v1, v100 being Element of L holds (v100 "\/" v1) "/\" (v100 "\/" ((v100 "\/" v1) "/\" v102)) = v100 "\/" ((v100 "\/" v1) "/\" v102)
A202:
for v0, v100, v1 being Element of L holds v100 "\/" (v0 "\/" (v1 "\/" v100)) = (v0 "\/" v1) "\/" v100
A205:
for v1, v0, v2 being Element of L holds v0 "\/" (v1 "\/" (v2 "\/" v0)) = v1 "\/" (v2 "\/" v0)
A208:
for v102, v100, v1 being Element of L holds (v1 "\/" v100) "/\" (v100 "\/" ((v1 "\/" v100) "/\" v102)) = v100 "\/" ((v1 "\/" v100) "/\" v102)
A212:
for v102, v1, v100 being Element of L holds (v100 "\/" (v100 "/\" v1)) "/\" v102 = v100 "/\" ((v100 "\/" (v100 "/\" v1)) "/\" v102)
A217:
for v1, v0 being Element of L holds (v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" ((v0 "/\" v1) "/\" ((v1 "/\" (v0 "/\" v1)) "\/" v0))) = ((v0 "/\" v1) "\/" ((v1 "\/" (v0 "/\" v1)) "/\" v0)) "/\" (v0 "\/" v1)
A219:
for v1, v0 being Element of L holds (v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" ((v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" v0))) = ((v0 "/\" v1) "\/" ((v1 "\/" (v0 "/\" v1)) "/\" v0)) "/\" (v0 "\/" v1)
A221:
for v1, v0 being Element of L holds (v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" ((v0 "/\" v1) "/\" (v0 "\/" (v0 "/\" v1)))) = ((v0 "/\" v1) "\/" ((v1 "\/" (v0 "/\" v1)) "/\" v0)) "/\" (v0 "\/" v1)
A223:
for v1, v0 being Element of L holds (v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" (v0 "/\" (v1 "/\" (v0 "\/" (v0 "/\" v1))))) = ((v0 "/\" v1) "\/" ((v1 "\/" (v0 "/\" v1)) "/\" v0)) "/\" (v0 "\/" v1)
A225:
for v1, v0 being Element of L holds (v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" (v0 "/\" v1)) = ((v0 "/\" v1) "\/" ((v1 "\/" (v0 "/\" v1)) "/\" v0)) "/\" (v0 "\/" v1)
A227:
for v1, v0 being Element of L holds (v0 "/\" v1) "/\" (v0 "/\" v1) = ((v0 "/\" v1) "\/" ((v1 "\/" (v0 "/\" v1)) "/\" v0)) "/\" (v0 "\/" v1)
A229:
for v1, v0 being Element of L holds v0 "/\" v1 = ((v0 "/\" v1) "\/" ((v1 "\/" (v0 "/\" v1)) "/\" v0)) "/\" (v0 "\/" v1)
A231:
for v1, v0 being Element of L holds v0 "/\" v1 = ((v0 "/\" v1) "\/" (v0 "/\" (v1 "\/" (v0 "/\" v1)))) "/\" (v0 "\/" v1)
A233:
for v1, v0 being Element of L holds v0 "/\" v1 = (v0 "/\" (v1 "\/" (v0 "/\" v1))) "/\" (v0 "\/" v1)
A235:
for v1, v0 being Element of L holds v0 "/\" v1 = v0 "/\" ((v1 "\/" (v0 "/\" v1)) "/\" (v0 "\/" v1))
A239:
for v100, v1, v101 being Element of L holds v100 "/\" (v101 "\/" (v101 "/\" v1)) = v101 "/\" (v100 "/\" (v101 "\/" (v101 "/\" v1)))
A244:
for v2, v1, v0 being Element of L holds (v0 "\/" (v0 "/\" v1)) "/\" (v1 "\/" v2) = v0 "/\" (v1 "\/" v2)
A246:
for v1, v0 being Element of L holds v1 "/\" (v0 "\/" (v0 "/\" v1)) = v0 "/\" v1
A249:
for v1, v0 being Element of L holds v0 "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" (v0 "/\" (v0 "\/" v1)))
A251:
for v1, v0 being Element of L holds v0 "/\" (v1 "\/" (v0 "/\" v1)) = v1 "/\" v0
A254:
for v1, v0 being Element of L holds ((v1 "/\" (v0 "/\" v1)) "\/" v0) "/\" (((v0 "/\" v1) "\/" ((v1 "\/" (v0 "/\" v1)) "/\" v0)) "/\" (v0 "\/" v1)) = (v0 "/\" v1) "/\" ((v1 "/\" (v0 "/\" v1)) "\/" v0)
A257:
for v0, v1 being Element of L holds ((v1 "/\" v0) "\/" v1) "/\" (((v1 "/\" v0) "\/" ((v0 "\/" (v1 "/\" v0)) "/\" v1)) "/\" (v1 "\/" v0)) = (v1 "/\" v0) "/\" ((v0 "/\" (v1 "/\" v0)) "\/" v1)
A260:
for v1, v0 being Element of L holds (v0 "\/" (v0 "/\" v1)) "/\" (((v0 "/\" v1) "\/" ((v1 "\/" (v0 "/\" v1)) "/\" v0)) "/\" (v0 "\/" v1)) = (v0 "/\" v1) "/\" ((v1 "/\" (v0 "/\" v1)) "\/" v0)
A262:
for v1, v0 being Element of L holds (v0 "\/" (v0 "/\" v1)) "/\" (((v0 "/\" v1) "\/" (v0 "/\" (v1 "\/" (v0 "/\" v1)))) "/\" (v0 "\/" v1)) = (v0 "/\" v1) "/\" ((v1 "/\" (v0 "/\" v1)) "\/" v0)
A264:
for v1, v0 being Element of L holds (v0 "\/" (v0 "/\" v1)) "/\" (((v0 "/\" v1) "\/" (v1 "/\" v0)) "/\" (v0 "\/" v1)) = (v0 "/\" v1) "/\" ((v1 "/\" (v0 "/\" v1)) "\/" v0)
A266:
for v1, v0 being Element of L holds (v0 "\/" (v0 "/\" v1)) "/\" ((v0 "\/" v1) "/\" ((v0 "/\" v1) "\/" (v1 "/\" v0))) = (v0 "/\" v1) "/\" ((v1 "/\" (v0 "/\" v1)) "\/" v0)
A268:
for v1, v0 being Element of L holds (v0 "\/" v1) "/\" ((v0 "\/" (v0 "/\" v1)) "/\" ((v0 "/\" v1) "\/" (v1 "/\" v0))) = (v0 "/\" v1) "/\" ((v1 "/\" (v0 "/\" v1)) "\/" v0)
A270:
for v1, v0 being Element of L holds (v0 "\/" v1) "/\" ((v0 "\/" (v0 "/\" v1)) "/\" ((v0 "/\" v1) "\/" (v1 "/\" v0))) = (v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" v0)
A272:
for v1, v0 being Element of L holds (v0 "\/" v1) "/\" ((v0 "\/" (v0 "/\" v1)) "/\" ((v0 "/\" v1) "\/" (v1 "/\" v0))) = (v0 "/\" v1) "/\" (v0 "\/" (v0 "/\" v1))
A274:
for v1, v0 being Element of L holds (v0 "\/" v1) "/\" ((v0 "\/" (v0 "/\" v1)) "/\" ((v0 "/\" v1) "\/" (v1 "/\" v0))) = v0 "/\" (v1 "/\" (v0 "\/" (v0 "/\" v1)))
A276:
for v1, v0 being Element of L holds (v0 "\/" v1) "/\" ((v0 "\/" (v0 "/\" v1)) "/\" ((v0 "/\" v1) "\/" (v1 "/\" v0))) = v0 "/\" (v0 "/\" v1)
A278:
for v1, v0 being Element of L holds (v0 "\/" v1) "/\" ((v0 "\/" (v0 "/\" v1)) "/\" ((v0 "/\" v1) "\/" (v1 "/\" v0))) = v0 "/\" v1
A281:
for v101, v100 being Element of L holds (v100 "/\" v101) "\/" (v101 "/\" v100) = v100 "/\" (v101 "\/" (v101 "/\" v100))
A284:
for v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v1 "/\" v0) = v1 "/\" v0
A286:
for v1, v0 being Element of L holds (v0 "\/" v1) "/\" ((v0 "\/" (v0 "/\" v1)) "/\" (v1 "/\" v0)) = v0 "/\" v1
A288:
for v1, v0 being Element of L holds (v0 "\/" v1) "/\" ((v1 "/\" v0) "/\" (v0 "\/" (v0 "/\" v1))) = v0 "/\" v1
A290:
for v1, v0 being Element of L holds (v0 "\/" v1) "/\" (v1 "/\" (v0 "/\" (v0 "\/" (v0 "/\" v1)))) = v0 "/\" v1
A292:
for v1, v0 being Element of L holds (v0 "\/" v1) "/\" (v1 "/\" (v0 "\/" (v0 "/\" v1))) = v0 "/\" v1
A294:
for v1, v0 being Element of L holds (v0 "\/" v1) "/\" (v0 "/\" v1) = v0 "/\" v1
A296:
for v1, v0 being Element of L holds (v0 "/\" v1) "/\" (v0 "\/" v1) = v0 "/\" v1
A298:
for v1, v0 being Element of L holds v0 "/\" (v1 "/\" (v0 "\/" v1)) = v0 "/\" v1
A301:
for v102, v100, v1 being Element of L holds (v1 "/\" v100) "/\" v102 = v100 "/\" ((v1 "\/" (v100 "/\" v1)) "/\" v102)
A304:
for v0, v2, v1 being Element of L holds v0 "/\" (v1 "/\" v2) = v1 "/\" ((v0 "\/" (v1 "/\" v0)) "/\" v2)
A308:
for v1, v0 being Element of L holds v1 "/\" (v0 "/\" (v0 "\/" v1)) = v0 "/\" v1
A312:
for v103, v100, v101, v1 being Element of L holds (v100 "\/" v101) "/\" ((v100 "\/" (v1 "/\" v101)) "/\" v103) = (v100 "\/" (v101 "/\" (v1 "/\" v101))) "/\" v103
A315:
for v3, v0, v1, v2 being Element of L holds (v0 "\/" v1) "/\" ((v0 "\/" (v2 "/\" v1)) "/\" v3) = (v0 "\/" (v2 "/\" v1)) "/\" v3
A318:
for v102, v100, v1 being Element of L holds (v1 "/\" v100) "/\" v102 = v100 "/\" ((v1 "/\" (v1 "\/" v100)) "/\" v102)
A321:
for v0, v2, v1 being Element of L holds v0 "/\" (v1 "/\" v2) = v1 "/\" ((v0 "/\" (v0 "\/" v1)) "/\" v2)
A323:
for v0, v2, v1 being Element of L holds v0 "/\" (v1 "/\" v2) = v1 "/\" (v0 "/\" ((v0 "\/" v1) "/\" v2))
A328:
for v0, v100, v1 being Element of L holds v100 "/\" ((v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" v100))) = (v0 "\/" v1) "/\" v100
A332:
for v102, v1, v100 being Element of L holds (v100 "/\" (v100 "\/" v1)) "\/" v102 = v100 "\/" ((v100 "/\" (v100 "\/" v1)) "\/" v102)
A337:
for v100, v1, v101 being Element of L holds v100 "\/" (v101 "/\" (v101 "\/" v1)) = v101 "\/" (v100 "\/" (v101 "/\" (v101 "\/" v1)))
A342:
for v2, v1, v0 being Element of L holds (v0 "/\" (v0 "\/" v1)) "\/" (v1 "/\" v2) = v0 "\/" (v1 "/\" v2)
A344:
for v1, v0 being Element of L holds v1 "\/" (v0 "/\" (v0 "\/" v1)) = v0 "\/" v1
A347:
for v1, v0 being Element of L holds v0 "\/" (v0 "/\" v1) = v0 "/\" (v0 "\/" v1)
A349:
for v2, v1, v0 being Element of L holds (v0 "/\" (v0 "\/" v1)) "/\" (v1 "\/" v2) = v0 "/\" (v1 "\/" v2)
A351:
for v2, v1, v0 being Element of L holds v0 "/\" ((v0 "\/" v1) "/\" (v1 "\/" v2)) = v0 "/\" (v1 "\/" v2)
A353:
for v0, v2, v1 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" (v0 "/\" (v0 "\/" (v1 "/\" v2)))) = (v0 "\/" (v0 "/\" v1)) "/\" (v2 "\/" (v0 "/\" ((v0 "/\" v1) "\/" v2)))
A355:
for v0, v2, v1 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" (v0 "/\" (v0 "\/" (v1 "/\" v2)))) = (v0 "/\" (v0 "\/" v1)) "/\" (v2 "\/" (v0 "/\" ((v0 "/\" v1) "\/" v2)))
A357:
for v0, v2, v1 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" (v0 "/\" (v0 "\/" (v1 "/\" v2)))) = v0 "/\" ((v0 "\/" v1) "/\" (v2 "\/" (v0 "/\" ((v0 "/\" v1) "\/" v2))))
A360:
for v101, v100 being Element of L holds (v100 "\/" v101) "/\" (v101 "\/" v100) = v100 "\/" (v101 "/\" (v101 "\/" v100))
A363:
for v1, v0 being Element of L holds (v0 "\/" v1) "/\" (v1 "\/" v0) = v1 "\/" v0
A366:
for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" ((v0 "/\" v1) "/\" (v0 "/\" (v1 "\/" v2))) = (v0 "/\" v1) "\/" (v0 "/\" (v1 "\/" v2))
A368:
for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" ((v0 "/\" v1) "/\" (v1 "\/" v2))) = (v0 "/\" v1) "\/" (v0 "/\" (v1 "\/" v2))
A370:
for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" (v0 "/\" (v1 "/\" (v1 "\/" v2)))) = (v0 "/\" v1) "\/" (v0 "/\" (v1 "\/" v2))
A372:
for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" (v1 "/\" (v1 "\/" v2))) = (v0 "/\" v1) "\/" (v0 "/\" (v1 "\/" v2))
A374:
for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" (v1 "/\" (v1 "\/" v2))) = v0 "/\" (v1 "\/" v2)
A377:
for v101, v1 being Element of L holds (v1 "\/" v101) "\/" (v101 "/\" (v1 "\/" v101)) = v101 "\/" (v1 "\/" v101)
A380:
for v1, v0 being Element of L holds v0 "\/" (v1 "\/" (v1 "/\" (v0 "\/" v1))) = v1 "\/" (v0 "\/" v1)
A382:
for v1, v0 being Element of L holds v0 "\/" (v1 "/\" (v1 "\/" (v0 "\/" v1))) = v1 "\/" (v0 "\/" v1)
A384:
for v1, v0 being Element of L holds v0 "\/" (v1 "/\" (v0 "\/" v1)) = v1 "\/" (v0 "\/" v1)
A386:
for v1, v0 being Element of L holds v0 "\/" (v1 "/\" (v0 "\/" v1)) = v0 "\/" v1
A389:
for v103, v100, v101 being Element of L holds (v100 "\/" v101) "/\" ((v101 "\/" v100) "/\" v103) = (v100 "\/" (v101 "/\" (v101 "\/" v100))) "/\" v103
A392:
for v2, v0, v1 being Element of L holds (v0 "\/" v1) "/\" ((v1 "\/" v0) "/\" v2) = (v1 "\/" v0) "/\" v2
A395:
for v0, v101, v1 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" (v1 "/\" v101)) = (v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" v101)
A398:
for v0, v2, v1 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" (v1 "/\" v2)) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2))
A400:
for v0, v1 being Element of L holds v0 "\/" (v1 "/\" v0) = v0 "/\" (v0 "\/" v1)
A403:
for v102, v1, v100 being Element of L holds (v100 "/\" (v100 "\/" v1)) "\/" v102 = v100 "\/" ((v100 "/\" v1) "\/" v102)
A407:
for v100, v1, v101 being Element of L holds (v100 "/\" v101) "\/" (v100 "/\" (v101 "/\" (v101 "\/" v1))) = v100 "/\" (v101 "\/" (v101 "/\" v1))
A410:
for v2, v1, v0 being Element of L holds v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" (v1 "\/" v2))) = v0 "/\" (v1 "\/" (v1 "/\" v2))
A412:
for v2, v1, v0 being Element of L holds v0 "/\" (v1 "/\" (v1 "\/" ((v0 "/\" v1) "\/" v2))) = v0 "/\" (v1 "\/" (v1 "/\" v2))
A414:
for v2, v1, v0 being Element of L holds v0 "/\" (v1 "/\" (v1 "\/" ((v0 "/\" v1) "\/" v2))) = v0 "/\" (v1 "/\" (v1 "\/" v2))
A417:
for v1, v2, v100 being Element of L holds v100 "\/" (v1 "/\" (v100 "/\" v2)) = v100 "/\" (v100 "\/" (v1 "/\" v2))
A421:
for v100, v1, v101 being Element of L holds v100 "\/" (v101 "/\" (v101 "\/" v1)) = v101 "\/" (v100 "\/" (v101 "/\" v1))
A426:
for v2, v1, v0 being Element of L holds v0 "\/" ((v0 "/\" v1) "\/" (v1 "/\" v2)) = v0 "\/" (v1 "/\" v2)
A429:
for v100, v102, v101 being Element of L holds (v100 "\/" v101) "/\" ((v101 "/\" v102) "\/" v100) = (v100 "\/" (v101 "/\" v102)) "/\" ((v101 "/\" v102) "\/" v100)
A432:
for v0, v2, v1 being Element of L holds (v0 "\/" v1) "/\" ((v1 "/\" v2) "\/" v0) = (v1 "/\" v2) "\/" v0
A435:
for v100, v101, v1, v0 being Element of L holds (v100 "\/" (v101 "/\" (v0 "\/" v1))) "/\" (v100 "\/" (v101 "/\" (v1 "\/" v0))) = v100 "\/" (v101 "/\" ((v0 "\/" v1) "/\" (v1 "\/" v0)))
A438:
for v0, v1, v3, v2 being Element of L holds (v0 "\/" (v1 "/\" (v2 "\/" v3))) "/\" (v0 "\/" (v1 "/\" (v3 "\/" v2))) = v0 "\/" (v1 "/\" (v3 "\/" v2))
A441:
for v0, v100, v1 being Element of L holds v100 "\/" (v0 "/\" (v1 "/\" v100)) = v100 "/\" (v100 "\/" (v0 "/\" v1))
A445:
for v1, v2, v101 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" (v101 "/\" v2)) = (v1 "/\" v2) "/\" ((v1 "/\" v2) "\/" v101)
A448:
for v0, v1, v2 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" (v2 "/\" v1)) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2))
A451:
for v100, v1, v101 being Element of L holds v100 "\/" (v101 "/\" (v101 "\/" v1)) = v101 "\/" (v100 "\/" (v1 "/\" v101))
A456:
for v0, v2, v1 being Element of L holds v0 "/\" ((v1 "\/" v2) "/\" ((v0 "/\" (v1 "\/" v2)) "\/" v1)) = v0 "/\" (v1 "\/" v2)
A458:
for v0, v2, v1 being Element of L holds v0 "/\" ((v1 "\/" v2) "/\" (v1 "\/" (v0 "/\" (v1 "\/" v2)))) = v0 "/\" (v1 "\/" v2)
A461:
for v0, v1, v102, v100 being Element of L holds v100 "/\" (v0 "/\" (v1 "/\" (v100 "/\" v102))) = (v0 "/\" v1) "/\" (v100 "/\" v102)
A464:
for v1, v2, v3, v0 being Element of L holds v0 "/\" (v1 "/\" (v2 "/\" (v0 "/\" v3))) = v1 "/\" (v2 "/\" (v0 "/\" v3))
A467:
for v101, v0, v100, v1 being Element of L holds v100 "/\" (v101 "/\" (v0 "/\" (v1 "/\" v100))) = v101 "/\" ((v0 "/\" v1) "/\" v100)
A470:
for v1, v2, v0, v3 being Element of L holds v0 "/\" (v1 "/\" (v2 "/\" (v3 "/\" v0))) = v1 "/\" (v2 "/\" (v3 "/\" v0))
A473:
for v101, v1, v102 being Element of L holds (v1 "/\" (v102 "\/" v1)) "/\" (v101 "/\" (v102 "/\" v1)) = v101 "/\" (v102 "/\" (v1 "/\" (v102 "\/" v1)))
A476:
for v2, v0, v1 being Element of L holds v0 "/\" ((v1 "\/" v0) "/\" (v2 "/\" (v1 "/\" v0))) = v2 "/\" (v1 "/\" (v0 "/\" (v1 "\/" v0)))
A478:
for v2, v0, v1 being Element of L holds (v1 "\/" v0) "/\" (v2 "/\" (v1 "/\" v0)) = v2 "/\" (v1 "/\" (v0 "/\" (v1 "\/" v0)))
A481:
for v2, v1, v0 being Element of L holds (v0 "\/" v1) "/\" (v2 "/\" (v0 "/\" v1)) = v2 "/\" (v0 "/\" v1)
A484:
for v0, v1, v102, v100 being Element of L holds v100 "\/" (v0 "\/" (v1 "\/" (v100 "\/" v102))) = (v0 "\/" v1) "\/" (v100 "\/" v102)
A487:
for v1, v2, v3, v0 being Element of L holds v0 "\/" (v1 "\/" (v2 "\/" (v0 "\/" v3))) = v1 "\/" (v2 "\/" (v0 "\/" v3))
A490:
for v101, v102, v1 being Element of L holds (v1 "/\" (v1 "\/" v102)) "\/" (v101 "\/" (v1 "\/" v102)) = v101 "\/" (v102 "\/" (v1 "/\" (v1 "\/" v102)))
A493:
for v2, v1, v0 being Element of L holds v0 "\/" ((v0 "/\" v1) "\/" (v2 "\/" (v0 "\/" v1))) = v2 "\/" (v1 "\/" (v0 "/\" (v0 "\/" v1)))
A495:
for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v2 "\/" (v0 "\/" v1)) = v2 "\/" (v1 "\/" (v0 "/\" (v0 "\/" v1)))
A497:
for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v2 "\/" (v0 "\/" v1)) = v2 "\/" (v0 "\/" v1)
A500:
for v1, v2, v0 being Element of L holds v1 "\/" (v0 "/\" v2) = (v1 "\/" (v0 "/\" v2)) "/\" (v0 "\/" v1)
A505:
for v102, v1, v100 being Element of L holds (v100 "\/" v1) "/\" ((v100 "\/" v1) "\/" (v100 "/\" v102)) = (v100 "\/" v1) "\/" (v100 "/\" v102)
A508:
for v1, v2, v0 being Element of L holds (v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" (v0 "/\" v2))) = (v0 "\/" v1) "\/" (v0 "/\" v2)
A510:
for v1, v2, v0 being Element of L holds (v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" (v0 "/\" v2))) = v0 "\/" (v1 "\/" (v0 "/\" v2))
A513:
for v0, v2, v1 being Element of L holds v0 "/\" (v1 "\/" v2) = ((v1 "\/" v2) "/\" v0) "\/" (v0 "/\" v1)
A517:
for v0, v1, v2 being Element of L holds (v0 "/\" v1) "\/" ((v2 "\/" v1) "/\" v0) = v0 "/\" (v1 "\/" v2)
A520:
for v101, v2, v1 being Element of L holds ((v101 "\/" v1) "/\" v101) "\/" ((v101 "\/" v1) "/\" ((v1 "/\" v2) "\/" v101)) = v101 "\/" (v1 "/\" v2)
A523:
for v0, v2, v1 being Element of L holds (v0 "/\" (v0 "\/" v1)) "\/" ((v0 "\/" v1) "/\" ((v1 "/\" v2) "\/" v0)) = v0 "\/" (v1 "/\" v2)
A525:
for v0, v2, v1 being Element of L holds (v0 "/\" (v0 "\/" v1)) "\/" ((v1 "/\" v2) "\/" v0) = v0 "\/" (v1 "/\" v2)
A527:
for v0, v2, v1 being Element of L holds v0 "\/" ((v0 "/\" v1) "\/" ((v1 "/\" v2) "\/" v0)) = v0 "\/" (v1 "/\" v2)
A529:
for v0, v2, v1 being Element of L holds (v0 "/\" v1) "\/" ((v1 "/\" v2) "\/" v0) = v0 "\/" (v1 "/\" v2)
A532:
for v100, v1, v102 being Element of L holds (v100 "/\" (v1 "/\" (v102 "\/" v1))) "\/" (v100 "/\" (v102 "\/" v1)) = v100 "/\" ((v1 "/\" (v102 "\/" v1)) "\/" v102)
A535:
for v0, v1, v2 being Element of L holds (v0 "/\" (v2 "\/" v1)) "\/" (v0 "/\" (v1 "/\" (v2 "\/" v1))) = v0 "/\" ((v1 "/\" (v2 "\/" v1)) "\/" v2)
A538:
for v0, v2, v1 being Element of L holds v0 "/\" ((v1 "\/" v2) "/\" ((v0 "/\" (v1 "\/" v2)) "\/" v2)) = v0 "/\" ((v2 "/\" (v1 "\/" v2)) "\/" v1)
A540:
for v0, v2, v1 being Element of L holds v0 "/\" ((v1 "\/" v2) "/\" (v2 "\/" (v0 "/\" (v1 "\/" v2)))) = v0 "/\" ((v2 "/\" (v1 "\/" v2)) "\/" v1)
A542:
for v0, v2, v1 being Element of L holds v0 "/\" ((v1 "\/" v2) "/\" (v2 "\/" (v0 "/\" (v1 "\/" v2)))) = v0 "/\" (v1 "\/" (v2 "/\" (v1 "\/" v2)))
A544:
for v0, v2, v1 being Element of L holds v0 "/\" ((v1 "\/" v2) "/\" (v2 "\/" (v0 "/\" (v1 "\/" v2)))) = v0 "/\" (v1 "\/" v2)
A547:
for v101, v1, v2 being Element of L holds ((v101 "\/" v1) "/\" v101) "\/" (v101 "\/" (v2 "/\" v1)) = (v101 "\/" v1) "/\" (v101 "\/" (v2 "/\" v1))
A550:
for v0, v1, v2 being Element of L holds (v0 "/\" (v0 "\/" v1)) "\/" (v0 "\/" (v2 "/\" v1)) = (v0 "\/" v1) "/\" (v0 "\/" (v2 "/\" v1))
A552:
for v2, v1, v0 being Element of L holds v0 "\/" ((v0 "/\" (v0 "\/" v1)) "\/" (v2 "/\" v1)) = (v0 "\/" v1) "/\" (v0 "\/" (v2 "/\" v1))
A554:
for v2, v1, v0 being Element of L holds v0 "\/" (v0 "\/" ((v0 "/\" v1) "\/" (v2 "/\" v1))) = (v0 "\/" v1) "/\" (v0 "\/" (v2 "/\" v1))
A556:
for v2, v1, v0 being Element of L holds v0 "\/" ((v0 "/\" v1) "\/" (v2 "/\" v1)) = (v0 "\/" v1) "/\" (v0 "\/" (v2 "/\" v1))
A558:
for v2, v1, v0 being Element of L holds v0 "\/" ((v0 "/\" v1) "\/" (v2 "/\" v1)) = v0 "\/" (v2 "/\" v1)
A561:
for v102, v1, v100 being Element of L holds (v100 "\/" v1) "/\" (v100 "\/" (v102 "/\" (v100 "\/" v1))) = v100 "\/" (v102 "/\" (v100 "\/" v1))
A565:
for v102, v100, v1 being Element of L holds (v1 "\/" v100) "/\" (v100 "\/" (v102 "/\" (v1 "\/" v100))) = v100 "\/" (v102 "/\" (v1 "\/" v100))
A568:
for v0, v2, v1 being Element of L holds v0 "/\" (v1 "\/" (v0 "/\" (v1 "\/" v2))) = v0 "/\" (v1 "\/" v2)
A570:
for v0, v2, v1 being Element of L holds v0 "/\" (v2 "\/" (v0 "/\" (v1 "\/" v2))) = v0 "/\" (v1 "\/" v2)
A574:
for v101, v1, v2, v102 being Element of L holds (v1 "/\" ((v1 "\/" v102) "/\" v2)) "/\" (v101 "/\" (v1 "/\" (v102 "/\" v2))) = v101 "/\" (v102 "/\" (v1 "/\" ((v1 "\/" v102) "/\" v2)))
A577:
for v3, v0, v2, v1 being Element of L holds v0 "/\" (((v0 "\/" v1) "/\" v2) "/\" (v3 "/\" (v0 "/\" (v1 "/\" v2)))) = v3 "/\" (v1 "/\" (v0 "/\" ((v0 "\/" v1) "/\" v2)))
A579:
for v3, v0, v2, v1 being Element of L holds v0 "/\" ((v0 "\/" v1) "/\" (v2 "/\" (v3 "/\" (v0 "/\" (v1 "/\" v2))))) = v3 "/\" (v1 "/\" (v0 "/\" ((v0 "\/" v1) "/\" v2)))
A581:
for v3, v0, v2, v1 being Element of L holds v0 "/\" ((v0 "\/" v1) "/\" (v3 "/\" (v0 "/\" (v1 "/\" v2)))) = v3 "/\" (v1 "/\" (v0 "/\" ((v0 "\/" v1) "/\" v2)))
A584:
for v2, v0, v3, v1 being Element of L holds (v0 "\/" v1) "/\" (v2 "/\" (v0 "/\" (v1 "/\" v3))) = v2 "/\" (v1 "/\" (v0 "/\" ((v0 "\/" v1) "/\" v3)))
A586:
for v2, v0, v3, v1 being Element of L holds (v0 "\/" v1) "/\" (v2 "/\" (v0 "/\" (v1 "/\" v3))) = v2 "/\" (v0 "/\" (v1 "/\" v3))
A589:
for v102, v1, v100 being Element of L holds v100 "/\" ((v100 "/\" (v100 "\/" v1)) "/\" ((v100 "/\" v1) "\/" v102)) = v100 "/\" ((v100 "/\" v1) "\/" v102)
A592:
for v2, v1, v0 being Element of L holds v0 "/\" (v0 "/\" ((v0 "\/" v1) "/\" ((v0 "/\" v1) "\/" v2))) = v0 "/\" ((v0 "/\" v1) "\/" v2)
A594:
for v2, v1, v0 being Element of L holds v0 "/\" ((v0 "\/" v1) "/\" ((v0 "/\" v1) "\/" v2)) = v0 "/\" ((v0 "/\" v1) "\/" v2)
A597:
for v100, v1, v2, v101 being Element of L holds v100 "/\" ((v100 "\/" v101) "/\" (v1 "\/" (v101 "\/" v2))) = v100 "/\" (v101 "\/" (v1 "\/" (v101 "\/" v2)))
A600:
for v0, v2, v3, v1 being Element of L holds v0 "/\" ((v0 "\/" v1) "/\" (v2 "\/" (v1 "\/" v3))) = v0 "/\" (v2 "\/" (v1 "\/" v3))
A603:
for v101, v1, v0 being Element of L holds v0 "\/" ((v0 "/\" v1) "\/" v101) = v101 "\/" (v0 "/\" (v0 "\/" v1))
A607:
for v101, v1, v0 being Element of L holds v0 "\/" ((v0 "/\" v1) "\/" ((v0 "/\" (v0 "\/" v1)) "/\" v101)) = (v0 "/\" (v0 "\/" v1)) "/\" ((v0 "/\" (v0 "\/" v1)) "\/" v101)
A610:
for v2, v1, v0 being Element of L holds v0 "\/" ((v0 "/\" v1) "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) = (v0 "/\" (v0 "\/" v1)) "/\" ((v0 "/\" (v0 "\/" v1)) "\/" v2)
A612:
for v2, v1, v0 being Element of L holds v0 "\/" ((v0 "/\" v1) "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) = (v0 "/\" (v0 "\/" v1)) "/\" (v0 "\/" ((v0 "/\" v1) "\/" v2))
A614:
for v2, v1, v0 being Element of L holds v0 "\/" ((v0 "/\" v1) "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) = v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" ((v0 "/\" v1) "\/" v2)))
A617:
for v101, v1, v0 being Element of L holds v0 "\/" ((v0 "/\" v1) "\/" (v101 "/\" (v0 "/\" (v0 "\/" v1)))) = (v0 "/\" (v0 "\/" v1)) "/\" ((v0 "/\" (v0 "\/" v1)) "\/" v101)
A620:
for v2, v1, v0 being Element of L holds v0 "\/" ((v0 "/\" v1) "\/" (v2 "/\" (v0 "/\" (v0 "\/" v1)))) = (v0 "/\" (v0 "\/" v1)) "/\" (v0 "\/" ((v0 "/\" v1) "\/" v2))
A622:
for v2, v1, v0 being Element of L holds v0 "\/" ((v0 "/\" v1) "\/" (v2 "/\" (v0 "/\" (v0 "\/" v1)))) = v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" ((v0 "/\" v1) "\/" v2)))
A625:
for v101, v0, v102, v1 being Element of L holds (v0 "/\" v1) "\/" (v101 "/\" (v0 "/\" (v1 "/\" v102))) = (v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" (v101 "/\" v102))
A628:
for v2, v0, v3, v1 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" (v0 "/\" (v1 "/\" v3))) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" (v2 "/\" v3)))
A631:
for v0, v1, v102, v100 being Element of L holds v100 "\/" (v0 "/\" (v1 "/\" (v100 "/\" v102))) = v100 "/\" (v100 "\/" ((v0 "/\" v1) "/\" v102))
A634:
for v1, v2, v3, v0 being Element of L holds v0 "\/" (v1 "/\" (v2 "/\" (v0 "/\" v3))) = v0 "/\" (v0 "\/" (v1 "/\" (v2 "/\" v3)))
A637:
for v1, v2, v102, v101 being Element of L holds ((v1 "/\" ((v101 "/\" v102) "/\" v2)) "/\" v101) "\/" (v102 "/\" ((v101 "/\" v102) "/\" ((v101 "/\" v102) "\/" (v1 "/\" v2)))) = (v102 "\/" ((v101 "\/" v102) "/\" (v1 "/\" ((v101 "/\" v102) "/\" v2)))) "/\" ((v1 "/\" ((v101 "/\" v102) "/\" v2)) "\/" v101)
A640:
for v0, v1, v3, v2 being Element of L holds ((v0 "/\" (v1 "/\" (v2 "/\" v3))) "/\" v1) "\/" (v2 "/\" ((v1 "/\" v2) "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3)))) = (v2 "\/" ((v1 "\/" v2) "/\" (v0 "/\" ((v1 "/\" v2) "/\" v3)))) "/\" ((v0 "/\" ((v1 "/\" v2) "/\" v3)) "\/" v1)
A642:
for v0, v1, v3, v2 being Element of L holds (v1 "/\" (v0 "/\" (v1 "/\" (v2 "/\" v3)))) "\/" (v2 "/\" ((v1 "/\" v2) "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3)))) = (v2 "\/" ((v1 "\/" v2) "/\" (v0 "/\" ((v1 "/\" v2) "/\" v3)))) "/\" ((v0 "/\" ((v1 "/\" v2) "/\" v3)) "\/" v1)
A645:
for v1, v0, v3, v2 being Element of L holds (v1 "/\" (v0 "/\" (v2 "/\" v3))) "\/" (v2 "/\" ((v0 "/\" v2) "/\" ((v0 "/\" v2) "\/" (v1 "/\" v3)))) = (v2 "\/" ((v0 "\/" v2) "/\" (v1 "/\" ((v0 "/\" v2) "/\" v3)))) "/\" ((v1 "/\" ((v0 "/\" v2) "/\" v3)) "\/" v0)
A648:
for v0, v1, v3, v2 being Element of L holds (v0 "/\" (v1 "/\" (v2 "/\" v3))) "\/" (v2 "/\" (v1 "/\" (v2 "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3))))) = (v2 "\/" ((v1 "\/" v2) "/\" (v0 "/\" ((v1 "/\" v2) "/\" v3)))) "/\" ((v0 "/\" ((v1 "/\" v2) "/\" v3)) "\/" v1)
A650:
for v0, v1, v3, v2 being Element of L holds (v0 "/\" (v1 "/\" (v2 "/\" v3))) "\/" (v1 "/\" (v2 "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3)))) = (v2 "\/" ((v1 "\/" v2) "/\" (v0 "/\" ((v1 "/\" v2) "/\" v3)))) "/\" ((v0 "/\" ((v1 "/\" v2) "/\" v3)) "\/" v1)
A652:
for v0, v1, v3, v2 being Element of L holds (v0 "/\" (v1 "/\" (v2 "/\" v3))) "\/" (v1 "/\" (v2 "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3)))) = (v2 "\/" ((v1 "\/" v2) "/\" (v0 "/\" (v1 "/\" (v2 "/\" v3))))) "/\" ((v0 "/\" ((v1 "/\" v2) "/\" v3)) "\/" v1)
A654:
for v0, v1, v3, v2 being Element of L holds (v0 "/\" (v1 "/\" (v2 "/\" v3))) "\/" (v1 "/\" (v2 "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3)))) = (v2 "\/" (v0 "/\" (v1 "/\" (v2 "/\" v3)))) "/\" ((v0 "/\" ((v1 "/\" v2) "/\" v3)) "\/" v1)
A656:
for v0, v1, v3, v2 being Element of L holds (v0 "/\" (v1 "/\" (v2 "/\" v3))) "\/" (v1 "/\" (v2 "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3)))) = (v2 "/\" (v2 "\/" (v0 "/\" (v1 "/\" v3)))) "/\" ((v0 "/\" ((v1 "/\" v2) "/\" v3)) "\/" v1)
A658:
for v0, v1, v3, v2 being Element of L holds (v0 "/\" (v1 "/\" (v2 "/\" v3))) "\/" (v1 "/\" (v2 "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3)))) = (v2 "/\" (v2 "\/" (v0 "/\" (v1 "/\" v3)))) "/\" ((v0 "/\" (v1 "/\" (v2 "/\" v3))) "\/" v1)
A660:
for v0, v1, v3, v2 being Element of L holds (v0 "/\" (v1 "/\" (v2 "/\" v3))) "\/" (v1 "/\" (v2 "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3)))) = (v2 "/\" (v2 "\/" (v0 "/\" (v1 "/\" v3)))) "/\" (v1 "\/" (v0 "/\" (v1 "/\" (v2 "/\" v3))))
A662:
for v0, v1, v3, v2 being Element of L holds (v0 "/\" (v1 "/\" (v2 "/\" v3))) "\/" (v1 "/\" (v2 "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3)))) = (v2 "/\" (v2 "\/" (v0 "/\" (v1 "/\" v3)))) "/\" (v1 "/\" (v1 "\/" (v0 "/\" (v2 "/\" v3))))
A664:
for v0, v1, v3, v2 being Element of L holds (v0 "/\" (v1 "/\" (v2 "/\" v3))) "\/" (v1 "/\" (v2 "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3)))) = v1 "/\" ((v2 "/\" (v2 "\/" (v0 "/\" (v1 "/\" v3)))) "/\" (v1 "\/" (v0 "/\" (v2 "/\" v3))))
A666:
for v0, v1, v3, v2 being Element of L holds (v0 "/\" (v1 "/\" (v2 "/\" v3))) "\/" (v1 "/\" (v2 "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3)))) = v1 "/\" (v2 "/\" ((v2 "\/" (v0 "/\" (v1 "/\" v3))) "/\" (v1 "\/" (v0 "/\" (v2 "/\" v3)))))
A669:
for v0, v100, v1 being Element of L holds v100 "\/" ((v100 "\/" ((v1 "\/" v100) "/\" v0)) "/\" (v0 "\/" v1)) = (v0 "/\" v1) "\/" (v100 "/\" (v100 "\/" ((v1 "/\" v100) "\/" v0)))
A675:
for v101, v1, v2, v100 being Element of L holds (v100 "/\" v101) "\/" (v101 "/\" (v1 "\/" (v100 "/\" (v100 "\/" v2)))) = v101 "/\" (v100 "\/" (v1 "\/" (v100 "/\" v2)))
A679:
for v101, v2, v100 being Element of L holds (v2 "\/" ((v100 "\/" v2) "/\" (v100 "\/" v101))) "/\" ((v100 "\/" v101) "\/" v100) = v100 "\/" ((v100 "/\" v101) "\/" (v2 "/\" ((v100 "/\" v2) "\/" (v100 "\/" v101))))
A682:
for v2, v0, v1 being Element of L holds (v0 "\/" ((v1 "\/" v0) "/\" (v1 "\/" v2))) "/\" (v1 "\/" (v1 "\/" v2)) = v1 "\/" ((v1 "/\" v2) "\/" (v0 "/\" ((v1 "/\" v0) "\/" (v1 "\/" v2))))
A684:
for v2, v0, v1 being Element of L holds (v0 "\/" ((v1 "\/" v0) "/\" (v1 "\/" v2))) "/\" (v1 "\/" v2) = v1 "\/" ((v1 "/\" v2) "\/" (v0 "/\" ((v1 "/\" v0) "\/" (v1 "\/" v2))))
A686:
for v2, v0, v1 being Element of L holds (v1 "\/" v2) "/\" (v0 "\/" ((v1 "\/" v0) "/\" (v1 "\/" v2))) = v1 "\/" ((v1 "/\" v2) "\/" (v0 "/\" ((v1 "/\" v0) "\/" (v1 "\/" v2))))
A689:
for v1, v2, v0 being Element of L holds (v0 "\/" v1) "/\" (v2 "\/" ((v0 "\/" v2) "/\" (v0 "\/" v1))) = v0 "\/" ((v0 "/\" v1) "\/" (v2 "/\" (v0 "\/" ((v0 "/\" v2) "\/" v1))))
A693:
for v102, v1, v100 being Element of L holds v100 "\/" (v100 "\/" ((v100 "/\" v1) "\/" ((v100 "\/" v1) "/\" v102))) = v100 "\/" ((v100 "\/" v1) "/\" v102)
A696:
for v2, v1, v0 being Element of L holds v0 "\/" ((v0 "/\" v1) "\/" ((v0 "\/" v1) "/\" v2)) = v0 "\/" ((v0 "\/" v1) "/\" v2)
A699:
for v100, v1, v102 being Element of L holds (v100 "/\" (v102 "\/" v1)) "\/" (v102 "/\" (v102 "\/" ((v102 "/\" v1) "\/" v100))) = (v102 "\/" (((v102 "\/" v1) "\/" v102) "/\" v100)) "/\" (v100 "\/" (v102 "\/" v1))
A702:
for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v1 "/\" (v1 "\/" ((v1 "/\" v2) "\/" v0))) = (v1 "\/" ((v1 "\/" (v1 "\/" v2)) "/\" v0)) "/\" (v0 "\/" (v1 "\/" v2))
A704:
for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v1 "/\" (v1 "\/" ((v1 "/\" v2) "\/" v0))) = (v1 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v0 "\/" (v1 "\/" v2))
A707:
for v102, v2, v101 being Element of L holds (v101 "/\" v2) "\/" (v102 "/\" (v101 "/\" v2)) = (v101 "/\" v2) "/\" ((v101 "/\" v2) "\/" (v101 "/\" v102))
A710:
for v2, v1, v0 being Element of L holds (v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" v2) = (v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" (v0 "/\" v2))
A712:
for v2, v1, v0 being Element of L holds v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2)) = (v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" (v0 "/\" v2))
A714:
for v2, v1, v0 being Element of L holds v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2)) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" (v0 "/\" v2)))
A717:
for v2, v1, v0 being Element of L holds (v1 "\/" v0) "/\" (v2 "/\" (v0 "/\" v1)) = v2 "/\" (v0 "/\" v1)
A721:
for v102, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v102 "/\" (v0 "/\" v1)) = (v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" ((v0 "\/" v1) "/\" v102))
A724:
for v2, v1, v0 being Element of L holds (v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" v2) = (v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" ((v0 "\/" v1) "/\" v2))
A726:
for v2, v1, v0 being Element of L holds v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2)) = (v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" ((v0 "\/" v1) "/\" v2))
A728:
for v2, v1, v0 being Element of L holds v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2)) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" ((v0 "\/" v1) "/\" v2)))
A732:
for v2, v100, v1, v0 being Element of L holds v100 "/\" ((v100 "\/" (v0 "/\" v1)) "/\" (v2 "\/" (v0 "\/" v1))) = v100 "/\" ((v0 "/\" v1) "\/" (v2 "\/" (v0 "\/" v1)))
A735:
for v3, v0, v2, v1 being Element of L holds v0 "/\" ((v0 "\/" (v1 "/\" v2)) "/\" (v3 "\/" (v1 "\/" v2))) = v0 "/\" (v3 "\/" (v1 "\/" v2))
A738:
for v102, v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" v102 = (v0 "\/" (v1 "/\" v2)) "/\" ((v1 "\/" v0) "/\" v102)
A743:
for v102, v1, v2, v100 being Element of L holds ((v1 "\/" (v100 "/\" (v100 "\/" v2))) "/\" v102) "\/" (v102 "/\" v100) = v102 "/\" (v100 "\/" (v1 "\/" (v100 "/\" v2)))
A747:
for v101, v1, v102 being Element of L holds (v102 "\/" v1) "\/" (v101 "/\" (v102 "\/" v1)) = (v102 "\/" v1) "\/" (v101 "/\" v102)
A750:
for v2, v1, v0 being Element of L holds (v0 "\/" v1) "/\" ((v0 "\/" v1) "\/" v2) = (v0 "\/" v1) "\/" (v2 "/\" v0)
A752:
for v0, v2, v1 being Element of L holds (v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" v2)) = (v0 "\/" v1) "\/" (v2 "/\" v0)
A754:
for v0, v2, v1 being Element of L holds (v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" v2)) = v0 "\/" (v1 "\/" (v2 "/\" v0))
A758:
for v102, v1, v100 being Element of L holds v100 "\/" (v102 "/\" (v100 "\/" v1)) = ((v100 "\/" v1) "/\" v102) "\/" (v100 "/\" (v100 "\/" v102))
A764:
for v102, v1, v2, v100 being Element of L holds ((v1 "\/" (v100 "/\" (v100 "\/" v2))) "/\" v102) "\/" (v102 "/\" v100) = v102 "/\" (v100 "\/" (v1 "\/" (v2 "/\" v100)))
A767:
for v3, v0, v2, v1 being Element of L holds v3 "/\" (v1 "\/" (v0 "\/" (v1 "/\" v2))) = v3 "/\" (v1 "\/" (v0 "\/" (v2 "/\" v1)))
A770:
for v0, v2, v3, v1 being Element of L holds v0 "/\" (v1 "\/" (v2 "\/" (v1 "/\" v3))) = v0 "/\" ((v1 "\/" v2) "/\" (v1 "\/" (v2 "\/" v3)))
A772:
for v1, v2, v3, v0 being Element of L holds (v0 "/\" v1) "\/" (v1 "/\" (v2 "\/" (v0 "/\" (v0 "\/" v3)))) = v1 "/\" ((v0 "\/" v2) "/\" (v0 "\/" (v2 "\/" v3)))
A774:
for v0, v2, v1 being Element of L holds (v0 "\/" v1) "/\" ((v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" v2))) = v0 "\/" (v1 "\/" (v0 "/\" v2))
A776:
for v0, v2, v1 being Element of L holds (v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" v2)) = v0 "\/" (v1 "\/" (v0 "/\" v2))
A779:
for v2, v1, v0 being Element of L holds (v0 "\/" (v0 "/\" v1)) "/\" (v0 "\/" ((v0 "/\" v1) "\/" ((v0 "\/" v1) "/\" v2))) = v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" ((v0 "/\" v1) "\/" v2)))
A781:
for v2, v1, v0 being Element of L holds (v0 "/\" (v0 "\/" v1)) "/\" (v0 "\/" ((v0 "/\" v1) "\/" ((v0 "\/" v1) "/\" v2))) = v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" ((v0 "/\" v1) "\/" v2)))
A783:
for v2, v1, v0 being Element of L holds (v0 "/\" (v0 "\/" v1)) "/\" (v0 "\/" ((v0 "\/" v1) "/\" v2)) = v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" ((v0 "/\" v1) "\/" v2)))
A785:
for v2, v1, v0 being Element of L holds v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" ((v0 "\/" v1) "/\" v2))) = v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" ((v0 "/\" v1) "\/" v2)))
A787:
for v2, v1, v0 being Element of L holds v0 "/\" (v0 "\/" ((v0 "\/" v1) "/\" v2)) = v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" ((v0 "/\" v1) "\/" v2)))
A790:
for v2, v1, v0 being Element of L holds v0 "\/" ((v0 "/\" v1) "\/" (v2 "/\" (v0 "/\" (v0 "\/" v1)))) = v0 "/\" (v0 "\/" ((v0 "\/" v1) "/\" v2))
A793:
for v102, v100, v1 being Element of L holds (v1 "/\" v100) "\/" ((v102 "\/" (v1 "/\" (v1 "\/" v100))) "/\" v100) = v100 "/\" ((v1 "/\" (v1 "\/" v100)) "\/" v102)
A796:
for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v1 "/\" (v2 "\/" (v0 "/\" (v0 "\/" v1)))) = v1 "/\" ((v0 "/\" (v0 "\/" v1)) "\/" v2)
A798:
for v0, v1, v2 being Element of L holds v1 "/\" ((v0 "\/" v2) "/\" (v0 "\/" (v2 "\/" v1))) = v1 "/\" ((v0 "/\" (v0 "\/" v1)) "\/" v2)
A801:
for v0, v2, v1 being Element of L holds (v1 "\/" v2) "/\" v0 = v0 "/\" ((v1 "/\" (v1 "\/" v0)) "\/" v2)
A804:
for v2, v1, v0 being Element of L holds (v0 "\/" v1) "/\" v2 = v2 "/\" (v0 "\/" ((v0 "/\" v2) "\/" v1))
A808:
for v2, v1, v0 being Element of L holds v0 "\/" ((v0 "/\" v1) "\/" ((v0 "\/" v1) "/\" v2)) = (v0 "\/" v1) "/\" (v2 "\/" ((v0 "\/" v2) "/\" (v0 "\/" v1)))
A810:
for v2, v1, v0 being Element of L holds v0 "\/" ((v0 "\/" v1) "/\" v2) = (v0 "\/" v1) "/\" (v2 "\/" ((v0 "\/" v2) "/\" (v0 "\/" v1)))
A813:
for v1, v2, v102, v101 being Element of L holds ((v1 "/\" ((v101 "/\" v102) "/\" v2)) "/\" v101) "\/" ((v101 "/\" v102) "/\" ((v101 "/\" v102) "\/" (v1 "/\" v2))) = (v1 "/\" ((v101 "/\" v102) "/\" v2)) "\/" (v101 "/\" v102)
A816:
for v0, v1, v3, v2 being Element of L holds ((v0 "/\" (v1 "/\" (v2 "/\" v3))) "/\" v1) "\/" ((v1 "/\" v2) "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3))) = (v0 "/\" ((v1 "/\" v2) "/\" v3)) "\/" (v1 "/\" v2)
A818:
for v0, v1, v3, v2 being Element of L holds (v1 "/\" (v0 "/\" (v1 "/\" (v2 "/\" v3)))) "\/" ((v1 "/\" v2) "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3))) = (v0 "/\" ((v1 "/\" v2) "/\" v3)) "\/" (v1 "/\" v2)
A821:
for v1, v0, v3, v2 being Element of L holds (v1 "/\" (v0 "/\" (v2 "/\" v3))) "\/" ((v0 "/\" v2) "/\" ((v0 "/\" v2) "\/" (v1 "/\" v3))) = (v1 "/\" ((v0 "/\" v2) "/\" v3)) "\/" (v0 "/\" v2)
A824:
for v0, v1, v3, v2 being Element of L holds (v0 "/\" (v1 "/\" (v2 "/\" v3))) "\/" (v1 "/\" (v2 "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3)))) = (v0 "/\" ((v1 "/\" v2) "/\" v3)) "\/" (v1 "/\" v2)
A826:
for v2, v0, v3, v1 being Element of L holds v1 "/\" (v2 "/\" ((v2 "\/" (v0 "/\" (v1 "/\" v3))) "/\" (v1 "\/" (v0 "/\" (v2 "/\" v3))))) = (v0 "/\" ((v1 "/\" v2) "/\" v3)) "\/" (v1 "/\" v2)
A829:
for v1, v2, v3, v0 being Element of L holds v0 "/\" (v1 "/\" ((v1 "\/" (v2 "/\" (v0 "/\" v3))) "/\" (v0 "\/" (v2 "/\" (v1 "/\" v3))))) = (v2 "/\" (v0 "/\" (v1 "/\" v3))) "\/" (v0 "/\" v1)
A831:
for v1, v2, v3, v0 being Element of L holds v0 "/\" (v1 "/\" ((v1 "\/" (v2 "/\" (v0 "/\" v3))) "/\" (v0 "\/" (v2 "/\" (v1 "/\" v3))))) = (v0 "/\" v1) "\/" (v2 "/\" (v0 "/\" (v1 "/\" v3)))
A833:
for v1, v2, v3, v0 being Element of L holds v0 "/\" (v1 "/\" ((v1 "\/" (v2 "/\" (v0 "/\" v3))) "/\" (v0 "\/" (v2 "/\" (v1 "/\" v3))))) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" (v2 "/\" v3)))
A836:
for v2, v1, v0 being Element of L holds v0 "/\" (v1 "/\" ((v1 "\/" ((v0 "\/" v1) "/\" (v0 "/\" v2))) "/\" (v0 "\/" ((v0 "\/" v1) "/\" (v1 "/\" v2))))) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2))
A838:
for v2, v1, v0 being Element of L holds v0 "/\" (v1 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "\/" ((v0 "\/" v1) "/\" (v1 "/\" v2))))) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2))
A840:
for v2, v1, v0 being Element of L holds v0 "/\" (v1 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "\/" (v1 "/\" ((v0 "\/" v1) "/\" v2))))) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2))
A843:
for v2, v1, v0 being Element of L holds v0 "/\" (v1 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" (v0 "/\" v2)))) "/\" (v0 "\/" (v1 "/\" ((v0 "\/" v1) "/\" (v0 "/\" v2)))))) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2))
A845:
for v2, v1, v0 being Element of L holds v0 "/\" (v1 "/\" ((v1 "\/" (v0 "/\" (v0 "/\" ((v0 "\/" v1) "/\" v2)))) "/\" (v0 "\/" (v1 "/\" ((v0 "\/" v1) "/\" (v0 "/\" v2)))))) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2))
A847:
for v2, v1, v0 being Element of L holds v0 "/\" (v1 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "\/" (v1 "/\" ((v0 "\/" v1) "/\" (v0 "/\" v2)))))) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2))
A849:
for v2, v1, v0 being Element of L holds v0 "/\" (v1 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "\/" (v1 "/\" (v0 "/\" ((v0 "\/" v1) "/\" v2)))))) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2))
A851:
for v2, v1, v0 being Element of L holds v0 "/\" (v1 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "\/" (v0 "/\" (v1 "/\" v2))))) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2))
A853:
for v2, v1, v0 being Element of L holds v0 "/\" (v1 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "/\" (v0 "\/" (v1 "/\" v2))))) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2))
A855:
for v2, v1, v0 being Element of L holds v0 "/\" (v1 "/\" (v0 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "\/" (v1 "/\" v2))))) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2))
A857:
for v2, v1, v0 being Element of L holds v1 "/\" (v0 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "\/" (v1 "/\" v2)))) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2))
A860:
for v2, v0, v1 being Element of L holds v0 "/\" (v1 "/\" ((v0 "\/" (v1 "/\" ((v1 "\/" v0) "/\" v2))) "/\" (v1 "\/" (v0 "/\" v2)))) = v1 "/\" (v0 "/\" ((v0 "\/" (v1 "/\" ((v1 "\/" v0) "/\" v2))) "/\" (v1 "\/" (v0 "/\" ((v1 "\/" v0) "/\" v2)))))
A864:
for v2, v1, v0 being Element of L holds v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2)) = v1 "/\" (v0 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "\/" (v1 "/\" v2))))
A867:
for v102, v1, v100 being Element of L holds v100 "\/" ((v100 "/\" v1) "\/" (v102 "/\" (v100 "/\" v1))) = v100 "\/" (v102 "/\" (v100 "/\" v1))
A870:
for v2, v1, v0 being Element of L holds v0 "\/" ((v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" v2)) = v0 "\/" (v2 "/\" (v0 "/\" v1))
A872:
for v2, v1, v0 being Element of L holds v0 "\/" (v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2))) = v0 "\/" (v2 "/\" (v0 "/\" v1))
A874:
for v2, v1, v0 being Element of L holds v0 "\/" (v1 "/\" (v0 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "\/" (v1 "/\" v2))))) = v0 "\/" (v2 "/\" (v0 "/\" v1))
A876:
for v2, v1, v0 being Element of L holds v0 "/\" (v0 "\/" (v1 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "\/" (v1 "/\" v2))))) = v0 "\/" (v2 "/\" (v0 "/\" v1))
A878:
for v2, v1, v0 being Element of L holds v0 "/\" (v0 "\/" (v1 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "\/" (v1 "/\" v2))))) = v0 "/\" (v0 "\/" (v2 "/\" v1))
A881:
for v102, v1, v100 being Element of L holds v100 "\/" (v100 "\/" ((v100 "/\" v1) "\/" (v102 "/\" (v100 "\/" v1)))) = v100 "\/" (v102 "/\" (v100 "\/" v1))
A884:
for v2, v1, v0 being Element of L holds v0 "\/" ((v0 "/\" v1) "\/" (v2 "/\" (v0 "\/" v1))) = v0 "\/" (v2 "/\" (v0 "\/" v1))
A887:
for v101, v2, v1 being Element of L holds (v1 "\/" (v101 "/\" (v1 "\/" v2))) "\/" (v101 "/\" (v1 "\/" v2)) = (v1 "\/" (v101 "/\" (v1 "\/" v2))) "/\" ((v1 "\/" (v101 "/\" (v1 "\/" v2))) "\/" v101)
A890:
for v1, v2, v0 being Element of L holds (v1 "/\" (v0 "\/" v2)) "\/" (v0 "\/" (v1 "/\" (v0 "\/" v2))) = (v0 "\/" (v1 "/\" (v0 "\/" v2))) "/\" ((v0 "\/" (v1 "/\" (v0 "\/" v2))) "\/" v1)
A893:
for v0, v2, v1 being Element of L holds v1 "\/" (v0 "/\" (v1 "\/" v2)) = (v1 "\/" (v0 "/\" (v1 "\/" v2))) "/\" ((v1 "\/" (v0 "/\" (v1 "\/" v2))) "\/" v0)
A896:
for v1, v2, v0 being Element of L holds v0 "\/" (v1 "/\" (v0 "\/" v2)) = (v0 "\/" (v1 "/\" (v0 "\/" v2))) "/\" (v1 "\/" (v0 "\/" (v1 "/\" (v0 "\/" v2))))
A898:
for v1, v2, v0 being Element of L holds v0 "\/" (v1 "/\" (v0 "\/" v2)) = (v0 "\/" (v1 "/\" (v0 "\/" v2))) "/\" ((v1 "\/" v0) "/\" (v1 "\/" (v0 "\/" (v0 "\/" v2))))
A900:
for v1, v2, v0 being Element of L holds v0 "\/" (v1 "/\" (v0 "\/" v2)) = (v0 "\/" (v1 "/\" (v0 "\/" v2))) "/\" ((v1 "\/" v0) "/\" (v1 "\/" (v0 "\/" v2)))
A902:
for v1, v2, v0 being Element of L holds v0 "\/" (v1 "/\" (v0 "\/" v2)) = (v0 "\/" (v1 "/\" (v0 "\/" v2))) "/\" (v1 "\/" (v0 "\/" v2))
A905:
for v0, v1, v2 being Element of L holds v0 "/\" (v1 "\/" ((v2 "\/" v1) "/\" v0)) = v0 "/\" (v2 "\/" v1)
A908:
for v100, v101, v1, v2 being Element of L holds v100 "/\" (v101 "/\" (v2 "\/" v1)) = v101 "/\" (v100 "/\" (v1 "\/" (v101 "/\" (v2 "\/" v1))))
A913:
for v2, v1, v0 being Element of L holds v0 "\/" ((v0 "\/" v1) "/\" v2) = (v0 "\/" v1) "/\" (v0 "\/" v2)
A915:
for v0, v2, v1 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" (v0 "/\" (v0 "\/" (v1 "/\" v2)))) = (v0 "\/" v1) "/\" (v0 "/\" ((v0 "/\" v1) "\/" v2))
A917:
for v0, v2, v1 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" (v0 "/\" (v0 "\/" (v1 "/\" v2)))) = v0 "/\" ((v0 "\/" v1) "/\" ((v0 "/\" v1) "\/" v2))
A919:
for v0, v2, v1 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" (v0 "/\" (v0 "\/" (v1 "/\" v2)))) = v0 "/\" ((v0 "/\" v1) "\/" v2)
A921:
for v2, v1, v0 being Element of L holds v0 "\/" ((v0 "/\" v1) "\/" (v2 "/\" (v0 "/\" (v0 "\/" v1)))) = v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" v2))
A923:
for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v1 "/\" (v1 "\/" ((v1 "/\" v2) "\/" v0))) = ((v1 "\/" v2) "/\" (v1 "\/" v0)) "/\" (v0 "\/" (v1 "\/" v2))
A925:
for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v1 "/\" (v1 "\/" ((v1 "/\" v2) "\/" v0))) = (v1 "\/" v2) "/\" ((v1 "\/" v0) "/\" (v0 "\/" (v1 "\/" v2)))
A927:
for v0, v2, v1 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" (v2 "\/" ((v1 "/\" v2) "\/" v0))) = (v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v2 "\/" (v0 "\/" v1))
A929:
for v2, v1, v0 being Element of L holds ((v0 "/\" v1) "\/" v2) "/\" ((v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v0 "\/" v1)) = (v2 "\/" ((v2 "\/" v1) "/\" v0)) "/\" (v0 "\/" v1)
A931:
for v0, v2, v1 being Element of L holds (v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v0 "\/" v1) = (v2 "\/" ((v2 "\/" v1) "/\" v0)) "/\" (v0 "\/" v1)
A934:
for v2, v0, v1 being Element of L holds (v0 "\/" ((v1 "\/" v0) "/\" v2)) "/\" (v2 "\/" v1) = ((v0 "\/" v1) "/\" (v0 "\/" v2)) "/\" (v2 "\/" v1)
A936:
for v2, v0, v1 being Element of L holds (v0 "\/" ((v1 "\/" v0) "/\" v2)) "/\" (v2 "\/" v1) = (v0 "\/" v1) "/\" ((v0 "\/" v2) "/\" (v2 "\/" v1))
A938:
for v2, v1, v0 being Element of L holds ((v0 "/\" v1) "\/" v2) "/\" ((v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v0 "\/" v1)) = (((v1 "\/" v2) "/\" v0) "\/" v2) "/\" (v0 "\/" v1)
A940:
for v2, v1, v0 being Element of L holds ((v0 "/\" v1) "\/" v2) "/\" ((v2 "\/" v1) "/\" ((v2 "\/" v0) "/\" (v0 "\/" v1))) = (((v1 "\/" v2) "/\" v0) "\/" v2) "/\" (v0 "\/" v1)
A942:
for v2, v1, v0 being Element of L holds ((v0 "/\" v1) "\/" v2) "/\" ((v2 "\/" v1) "/\" ((v2 "\/" v0) "/\" (v0 "\/" v1))) = (v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v0 "\/" v1)
A944:
for v2, v1, v0 being Element of L holds ((v0 "/\" v1) "\/" v2) "/\" ((v2 "\/" v1) "/\" ((v2 "\/" v0) "/\" (v0 "\/" v1))) = (v2 "\/" v1) "/\" ((v2 "\/" v0) "/\" (v0 "\/" v1))
A947:
for v100, v1, v0 being Element of L holds (v100 "\/" (v0 "/\" v1)) "/\" ((v100 "\/" ((v1 "\/" v100) "/\" v0)) "/\" (v0 "\/" v1)) = ((v0 "/\" v1) "\/" v100) "/\" ((v100 "\/" ((v1 "\/" v100) "/\" v0)) "/\" (v0 "\/" v1))
A950:
for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" ((v0 "\/" v2) "/\" ((v0 "\/" v1) "/\" (v1 "\/" v2))) = ((v1 "/\" v2) "\/" v0) "/\" ((v0 "\/" ((v2 "\/" v0) "/\" v1)) "/\" (v1 "\/" v2))
A952:
for v0, v2, v1 being Element of L holds (v0 "\/" v2) "/\" ((v0 "\/" (v1 "/\" v2)) "/\" ((v0 "\/" v1) "/\" (v1 "\/" v2))) = ((v1 "/\" v2) "\/" v0) "/\" ((v0 "\/" ((v2 "\/" v0) "/\" v1)) "/\" (v1 "\/" v2))
A955:
for v0, v1, v2 being Element of L holds (v0 "\/" v1) "/\" ((v0 "\/" v2) "/\" ((v0 "\/" (v2 "/\" v1)) "/\" (v2 "\/" v1))) = ((v2 "/\" v1) "\/" v0) "/\" ((v0 "\/" ((v1 "\/" v0) "/\" v2)) "/\" (v2 "\/" v1))
A957:
for v0, v1, v2 being Element of L holds (v0 "\/" v1) "/\" ((v0 "\/" (v2 "/\" v1)) "/\" (v2 "\/" v1)) = ((v2 "/\" v1) "\/" v0) "/\" ((v0 "\/" ((v1 "\/" v0) "/\" v2)) "/\" (v2 "\/" v1))
A959:
for v0, v1, v2 being Element of L holds (v0 "\/" (v2 "/\" v1)) "/\" (v2 "\/" v1) = ((v2 "/\" v1) "\/" v0) "/\" ((v0 "\/" ((v1 "\/" v0) "/\" v2)) "/\" (v2 "\/" v1))
A962:
for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v1 "\/" v2) = ((v1 "/\" v2) "\/" v0) "/\" ((v0 "\/" v2) "/\" ((v0 "\/" v1) "/\" (v1 "\/" v2)))
A964:
for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v1 "\/" v2) = (v0 "\/" v2) "/\" ((v0 "\/" v1) "/\" (v1 "\/" v2))
A966:
for v1, v2, v0 being Element of L holds (v0 "\/" (v0 "\/" v2)) "/\" ((v0 "\/" v1) "/\" (v1 "\/" (v0 "\/" v2))) = v0 "\/" (v1 "/\" (v0 "\/" v2))
A969:
for v2, v1, v0 being Element of L holds (v0 "\/" v1) "/\" ((v0 "\/" v2) "/\" (v2 "\/" (v0 "\/" v1))) = v0 "\/" (v2 "/\" (v0 "\/" v1))
A974:
for v1, v101, v100 being Element of L holds v100 "\/" ((v100 "/\" v101) "/\" ((v100 "/\" v101) "\/" v1)) = ((v100 "/\" v101) "/\" v1) "\/" (v100 "/\" (v100 "\/" v101))
A977:
for v2, v1, v0 being Element of L holds v0 "\/" (v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2))) = ((v0 "/\" v1) "/\" v2) "\/" (v0 "/\" (v0 "\/" v1))
A979:
for v2, v1, v0 being Element of L holds v0 "\/" (v1 "/\" (v0 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "\/" (v1 "/\" v2))))) = ((v0 "/\" v1) "/\" v2) "\/" (v0 "/\" (v0 "\/" v1))
A981:
for v2, v1, v0 being Element of L holds v0 "/\" (v0 "\/" (v1 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "\/" (v1 "/\" v2))))) = ((v0 "/\" v1) "/\" v2) "\/" (v0 "/\" (v0 "\/" v1))
A983:
for v0, v1, v2 being Element of L holds v0 "/\" (v0 "\/" (v2 "/\" v1)) = ((v0 "/\" v1) "/\" v2) "\/" (v0 "/\" (v0 "\/" v1))
A986:
for v0, v2, v1 being Element of L holds v0 "/\" (v0 "\/" (v1 "/\" v2)) = (v0 "/\" (v2 "/\" v1)) "\/" (v0 "/\" (v0 "\/" v2))
A991:
for v100, v1, v102 being Element of L holds v100 "\/" (v102 "\/" ((v102 "/\" v1) "\/" (v100 "/\" (v102 "\/" v1)))) = v100 "\/" (v102 "/\" (v102 "\/" v1))
A994:
for v0, v2, v1 being Element of L holds v0 "\/" (v1 "\/" (v0 "/\" (v1 "\/" v2))) = v0 "\/" (v1 "/\" (v1 "\/" v2))
A996:
for v0, v2, v1 being Element of L holds (v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" (v1 "\/" v2))) = v0 "\/" (v1 "/\" (v1 "\/" v2))
A998:
for v0, v2, v1 being Element of L holds (v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" v2)) = v0 "\/" (v1 "/\" (v1 "\/" v2))
A1001:
for v0, v2, v1 being Element of L holds ((v0 "/\" (v1 "/\" v2)) "\/" v0) "/\" ((v0 "/\" (v1 "/\" v2)) "\/" (v0 "\/" v1)) = v0 "/\" (v0 "\/" (v2 "/\" v1))
A1003:
for v0, v2, v1 being Element of L holds (v0 "\/" (v0 "/\" (v1 "/\" v2))) "/\" ((v0 "/\" (v1 "/\" v2)) "\/" (v0 "\/" v1)) = v0 "/\" (v0 "\/" (v2 "/\" v1))
A1005:
for v0, v2, v1 being Element of L holds (v0 "/\" (v0 "\/" (v1 "/\" v2))) "/\" ((v0 "/\" (v1 "/\" v2)) "\/" (v0 "\/" v1)) = v0 "/\" (v0 "\/" (v2 "/\" v1))
A1007:
for v0, v2, v1 being Element of L holds (v0 "/\" (v0 "\/" (v1 "/\" v2))) "/\" (v0 "\/" ((v0 "/\" (v1 "/\" v2)) "\/" v1)) = v0 "/\" (v0 "\/" (v2 "/\" v1))
A1009:
for v0, v2, v1 being Element of L holds (v0 "/\" (v0 "\/" (v1 "/\" v2))) "/\" (v0 "\/" (v1 "\/" (v0 "/\" (v1 "/\" v2)))) = v0 "/\" (v0 "\/" (v2 "/\" v1))
A1011:
for v0, v2, v1 being Element of L holds (v0 "/\" (v0 "\/" (v1 "/\" v2))) "/\" (v0 "\/" (v1 "/\" (v1 "\/" (v0 "/\" v2)))) = v0 "/\" (v0 "\/" (v2 "/\" v1))
A1013:
for v0, v2, v1 being Element of L holds (v0 "/\" (v0 "\/" (v1 "/\" v2))) "/\" ((v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" (v0 "/\" v2)))) = v0 "/\" (v0 "\/" (v2 "/\" v1))
A1015:
for v0, v2, v1 being Element of L holds (v0 "/\" (v0 "\/" (v1 "/\" v2))) "/\" ((v0 "\/" v1) "/\" ((v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" v2)))) = v0 "/\" (v0 "\/" (v2 "/\" v1))
A1017:
for v0, v2, v1 being Element of L holds (v0 "/\" (v0 "\/" (v1 "/\" v2))) "/\" ((v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" v2))) = v0 "/\" (v0 "\/" (v2 "/\" v1))
A1019:
for v0, v2, v1 being Element of L holds (v0 "\/" v1) "/\" ((v0 "/\" (v0 "\/" (v1 "/\" v2))) "/\" (v0 "\/" (v1 "\/" v2))) = v0 "/\" (v0 "\/" (v2 "/\" v1))
A1021:
for v0, v2, v1 being Element of L holds (v0 "\/" v1) "/\" (v0 "/\" ((v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" (v1 "\/" v2)))) = v0 "/\" (v0 "\/" (v2 "/\" v1))
A1023:
for v0, v2, v1 being Element of L holds (v0 "\/" v1) "/\" (v0 "/\" (v0 "\/" (v1 "\/" v2))) = v0 "/\" (v0 "\/" (v2 "/\" v1))
A1025:
for v0, v2, v1 being Element of L holds v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" v2))) = v0 "/\" (v0 "\/" (v2 "/\" v1))
A1027:
for v0, v2, v1 being Element of L holds v0 "/\" (v0 "\/" (v1 "\/" v2)) = v0 "/\" (v0 "\/" (v2 "/\" v1))
A1029:
for v0, v2, v1 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" (v2 "\/" (v0 "/\" (v1 "/\" v2)))) = (v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v2 "\/" (v0 "\/" v1))
A1031:
for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" (v2 "/\" (v2 "\/" (v0 "/\" v1)))) = (v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v2 "\/" (v0 "\/" v1))
A1033:
for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" (v2 "\/" (v0 "/\" v1))) = (v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v2 "\/" (v0 "\/" v1))
A1035:
for v2, v1, v0 being Element of L holds v2 "\/" (v0 "/\" v1) = (v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v2 "\/" (v0 "\/" v1))
A1040:
for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v1 "/\" (v1 "\/" (v0 "/\" (v1 "/\" v2)))) = (v1 "\/" v2) "/\" ((v1 "\/" v0) "/\" (v0 "\/" (v1 "\/" v2)))
A1042:
for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v1 "/\" (v1 "/\" (v1 "\/" (v0 "/\" v2)))) = (v1 "\/" v2) "/\" ((v1 "\/" v0) "/\" (v0 "\/" (v1 "\/" v2)))
A1044:
for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v1 "/\" (v1 "\/" (v0 "/\" v2))) = (v1 "\/" v2) "/\" ((v1 "\/" v0) "/\" (v0 "\/" (v1 "\/" v2)))
A1046:
for v0, v2, v1 being Element of L holds ((v0 "/\" (v1 "\/" v2)) "\/" v1) "/\" ((v0 "/\" (v1 "\/" v2)) "\/" (v1 "\/" (v0 "/\" v2))) = (v1 "\/" v2) "/\" ((v1 "\/" v0) "/\" (v0 "\/" (v1 "\/" v2)))
A1048:
for v0, v2, v1 being Element of L holds (v1 "\/" (v0 "/\" (v1 "\/" v2))) "/\" ((v0 "/\" (v1 "\/" v2)) "\/" (v1 "\/" (v0 "/\" v2))) = (v1 "\/" v2) "/\" ((v1 "\/" v0) "/\" (v0 "\/" (v1 "\/" v2)))
A1051:
for v1, v2, v0 being Element of L holds (v0 "\/" (v1 "/\" (v0 "\/" v2))) "/\" (v0 "\/" ((v1 "/\" (v0 "\/" v2)) "\/" (v1 "/\" v2))) = (v0 "\/" v2) "/\" ((v0 "\/" v1) "/\" (v1 "\/" (v0 "\/" v2)))
A1053:
for v1, v2, v0 being Element of L holds (v0 "\/" (v1 "/\" (v0 "\/" v2))) "/\" (v0 "\/" ((v1 "/\" v2) "\/" (v1 "/\" (v0 "\/" v2)))) = (v0 "\/" v2) "/\" ((v0 "\/" v1) "/\" (v1 "\/" (v0 "\/" v2)))
A1055:
for v1, v2, v0 being Element of L holds (v0 "\/" (v1 "/\" (v0 "\/" v2))) "/\" (v0 "\/" (v1 "/\" (v2 "\/" v0))) = (v0 "\/" v2) "/\" ((v0 "\/" v1) "/\" (v1 "\/" (v0 "\/" v2)))
A1057:
for v1, v0, v2 being Element of L holds v0 "\/" (v1 "/\" (v2 "\/" v0)) = (v0 "\/" v2) "/\" ((v0 "\/" v1) "/\" (v1 "\/" (v0 "\/" v2)))
A1059:
for v2, v1, v0 being Element of L holds (((v0 "\/" v1) "/\" v2) "\/" v0) "/\" (((v0 "\/" v1) "/\" v2) "\/" (v0 "\/" v2)) = v0 "\/" (v2 "/\" (v0 "\/" v1))
A1061:
for v2, v1, v0 being Element of L holds (v0 "\/" ((v0 "\/" v1) "/\" v2)) "/\" (((v0 "\/" v1) "/\" v2) "\/" (v0 "\/" v2)) = v0 "\/" (v2 "/\" (v0 "\/" v1))
A1063:
for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" (v0 "\/" v2)) "/\" (((v0 "\/" v1) "/\" v2) "\/" (v0 "\/" v2)) = v0 "\/" (v2 "/\" (v0 "\/" v1))
A1065:
for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" (v0 "\/" v2)) "/\" (v0 "\/" (((v0 "\/" v1) "/\" v2) "\/" v2)) = v0 "\/" (v2 "/\" (v0 "\/" v1))
A1067:
for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" (v0 "\/" v2)) "/\" (v0 "\/" (v2 "\/" ((v0 "\/" v1) "/\" v2))) = v0 "\/" (v2 "/\" (v0 "\/" v1))
A1069:
for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" (v0 "\/" v2)) "/\" (v0 "\/" (v2 "/\" (v2 "\/" (v0 "\/" v1)))) = v0 "\/" (v2 "/\" (v0 "\/" v1))
A1071:
for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" (v0 "\/" v2)) "/\" (v0 "\/" (v2 "/\" (v2 "\/" (v1 "/\" v0)))) = v0 "\/" (v2 "/\" (v0 "\/" v1))
A1073:
for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" (v0 "\/" v2)) "/\" ((v0 "\/" v2) "/\" (v0 "\/" (v2 "\/" (v1 "/\" v0)))) = v0 "\/" (v2 "/\" (v0 "\/" v1))
A1075:
for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" (v0 "\/" v2)) "/\" ((v0 "\/" v2) "/\" ((v0 "\/" v2) "/\" (v0 "\/" (v2 "\/" v1)))) = v0 "\/" (v2 "/\" (v0 "\/" v1))
A1077:
for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" (v0 "\/" v2)) "/\" ((v0 "\/" v2) "/\" (v0 "\/" (v2 "\/" v1))) = v0 "\/" (v2 "/\" (v0 "\/" v1))
A1079:
for v2, v1, v0 being Element of L holds (v0 "\/" v2) "/\" (((v0 "\/" v1) "/\" (v0 "\/" v2)) "/\" (v0 "\/" (v2 "\/" v1))) = v0 "\/" (v2 "/\" (v0 "\/" v1))
A1082:
for v0, v2, v1 being Element of L holds (v0 "\/" v1) "/\" ((v0 "\/" v2) "/\" ((v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" v2)))) = v0 "\/" (v1 "/\" (v0 "\/" v2))
A1084:
for v0, v2, v1 being Element of L holds (v0 "\/" v2) "/\" ((v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" v2))) = v0 "\/" (v1 "/\" (v0 "\/" v2))
A1089:
for v2, v1, v0 being Element of L holds v0 "/\" (v1 "/\" (v1 "\/" (v2 "/\" (v0 "/\" v1)))) = v0 "/\" (v1 "/\" (v1 "\/" v2))
A1091:
for v1, v0, v2 being Element of L holds v0 "/\" (v1 "/\" (v1 "/\" (v1 "\/" (v2 "/\" v0)))) = v0 "/\" (v1 "/\" (v1 "\/" v2))
A1093:
for v1, v0, v2 being Element of L holds v0 "/\" (v1 "/\" (v1 "\/" (v2 "/\" v0))) = v0 "/\" (v1 "/\" (v1 "\/" v2))
A1095:
for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" (v0 "/\" (v0 "\/" v1))) = v0 "/\" ((v0 "/\" v1) "\/" v2)
A1097:
for v2, v1, v0 being Element of L holds v0 "\/" (v0 "/\" ((v0 "/\" v1) "\/" v2)) = v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" v2))
A1099:
for v2, v1, v0 being Element of L holds v0 "/\" (v0 "\/" ((v0 "/\" v1) "\/" v2)) = v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" v2))
A1101:
for v2, v1, v0 being Element of L holds v0 "/\" (v0 "\/" (v2 "/\" (v0 "/\" v1))) = v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" v2))
A1104:
for v0, v2, v1 being Element of L holds v0 "/\" (v0 "/\" (v0 "\/" (v1 "/\" v2))) = v0 "/\" ((v0 "\/" v2) "/\" (v0 "\/" v1))
A1106:
for v0, v2, v1 being Element of L holds v0 "/\" (v0 "\/" (v1 "/\" v2)) = v0 "/\" ((v0 "\/" v2) "/\" (v0 "\/" v1))
A1108:
for v0, v2, v1 being Element of L holds v0 "/\" (v0 "\/" (v1 "\/" v2)) = v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" v2))
A1111:
for v100, v0, v1 being Element of L holds (v100 "\/" (v1 "\/" v0)) "/\" ((v1 "\/" v0) "/\" v100) = (v0 "\/" v1) "/\" ((v1 "\/" v0) "/\" v100)
A1114:
for v0, v2, v1 being Element of L holds ((v1 "\/" v2) "/\" v0) "/\" (v0 "\/" (v1 "\/" v2)) = (v2 "\/" v1) "/\" ((v1 "\/" v2) "/\" v0)
A1117:
for v2, v1, v0 being Element of L holds (v0 "\/" v1) "/\" (v2 "/\" (v2 "\/" (v0 "\/" v1))) = (v1 "\/" v0) "/\" ((v0 "\/" v1) "/\" v2)
A1119:
for v1, v0, v2 being Element of L holds (v0 "\/" v1) "/\" (v2 "/\" ((v2 "\/" v0) "/\" (v2 "\/" v1))) = (v1 "\/" v0) "/\" ((v0 "\/" v1) "/\" v2)
A1121:
for v1, v0, v2 being Element of L holds (v0 "\/" v1) "/\" (v2 "/\" ((v2 "\/" v0) "/\" (v2 "\/" v1))) = (v0 "\/" v1) "/\" v2
A1123:
for v2, v0, v1 being Element of L holds (v0 "\/" v1) "/\" (v1 "\/" ((v1 "\/" v0) "/\" v2)) = v1 "\/" ((v0 "\/" v1) "/\" v2)
A1125:
for v2, v0, v1 being Element of L holds (v0 "\/" v1) "/\" ((v1 "\/" v0) "/\" (v1 "\/" v2)) = v1 "\/" ((v0 "\/" v1) "/\" v2)
A1127:
for v2, v0, v1 being Element of L holds (v1 "\/" v0) "/\" (v1 "\/" v2) = v1 "\/" ((v0 "\/" v1) "/\" v2)
A1132:
for v1, v101, v100 being Element of L holds (v100 "\/" v101) "/\" (v101 "\/" (v1 "/\" (v100 "\/" v101))) = v101 "\/" ((v100 "\/" v101) "/\" (v1 "/\" (v1 "\/" (v100 "\/" v101))))
A1135:
for v2, v1, v0 being Element of L holds v1 "\/" (v2 "/\" (v0 "\/" v1)) = v1 "\/" ((v0 "\/" v1) "/\" (v2 "/\" (v2 "\/" (v0 "\/" v1))))
A1138:
for v1, v0, v2 being Element of L holds v0 "\/" (v1 "/\" (v2 "\/" v0)) = v0 "\/" ((v2 "\/" v0) "/\" (v1 "/\" ((v1 "\/" v2) "/\" (v1 "\/" v0))))
A1140:
for v1, v0, v2 being Element of L holds v0 "\/" (v1 "/\" (v2 "\/" v0)) = v0 "\/" ((v2 "\/" v0) "/\" v1)
A1142:
for v1, v0, v2 being Element of L holds v0 "\/" (v1 "/\" (v2 "\/" v0)) = (v0 "\/" v2) "/\" (v0 "\/" v1)
A1144:
for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" (v0 "\/" v2)) "/\" (v0 "\/" (v2 "\/" v1)) = v0 "\/" (v2 "/\" v1)
A1146:
for v0, v1, v2 being Element of L holds (v0 "\/" v1) "/\" ((v0 "\/" v2) "/\" (v0 "\/" (v2 "\/" v1))) = v0 "\/" (v2 "/\" v1)
A1148:
for v1, v2, v0 being Element of L holds (v0 "\/" v2) "/\" (v0 "\/" v1) = (v0 "\/" v2) "/\" ((v0 "\/" v1) "/\" (v1 "\/" (v0 "\/" v2)))
A1152:
for v1, v2, v0 being Element of L holds v0 "\/" (v1 "/\" (v0 "\/" v2)) = v0 "\/" (v1 "/\" v2)
A1154:
for v0, v2, v1 being Element of L holds v0 "\/" (v1 "/\" v2) = (v0 "\/" v2) "/\" ((v0 "\/" v1) "/\" (v1 "\/" (v0 "\/" v2)))
Z:
for v0, v2, v1 being Element of L holds v0 "\/" (v1 "/\" v2) = (v0 "\/" v2) "/\" (v0 "\/" v1)
let v1, v2, v3 be Element of L; v1 "\/" (v2 "/\" v3) = (v1 "\/" v2) "/\" (v1 "\/" v3)
v1 "\/" (v2 "/\" v3) = (v1 "\/" v3) "/\" (v1 "\/" v2)
by Z;
hence
v1 "\/" (v2 "/\" v3) = (v1 "\/" v2) "/\" (v1 "\/" v3)
by A4; verum