let L be non empty LattStr ; ( L is satisfying_McKenzie_1 & L is satisfying_McKenzie_2 & ( for v2, v1, v0 being Element of L holds ((v0 "/\" v1) "\/" (v1 "/\" v2)) "\/" v1 = v1 ) & ( for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" (v1 "\/" v2)) "/\" v1 = v1 ) implies ( ( for v1, v0 being Element of L holds v0 "/\" (v0 "\/" v1) = v0 ) & ( for v1, v0 being Element of L holds v0 "\/" (v0 "/\" v1) = v0 ) & L is join-commutative & L is meet-commutative & L is meet-associative & L is join-associative ) )
assume A2:
L is satisfying_McKenzie_1
; ( not L is satisfying_McKenzie_2 or ex v2, v1, v0 being Element of L st not ((v0 "/\" v1) "\/" (v1 "/\" v2)) "\/" v1 = v1 or ex v2, v1, v0 being Element of L st not ((v0 "\/" v1) "/\" (v1 "\/" v2)) "/\" v1 = v1 or ( ( for v1, v0 being Element of L holds v0 "/\" (v0 "\/" v1) = v0 ) & ( for v1, v0 being Element of L holds v0 "\/" (v0 "/\" v1) = v0 ) & L is join-commutative & L is meet-commutative & L is meet-associative & L is join-associative ) )
assume A3:
L is satisfying_McKenzie_2
; ( ex v2, v1, v0 being Element of L st not ((v0 "/\" v1) "\/" (v1 "/\" v2)) "\/" v1 = v1 or ex v2, v1, v0 being Element of L st not ((v0 "\/" v1) "/\" (v1 "\/" v2)) "/\" v1 = v1 or ( ( for v1, v0 being Element of L holds v0 "/\" (v0 "\/" v1) = v0 ) & ( for v1, v0 being Element of L holds v0 "\/" (v0 "/\" v1) = v0 ) & L is join-commutative & L is meet-commutative & L is meet-associative & L is join-associative ) )
assume A4:
for v2, v1, v0 being Element of L holds ((v0 "/\" v1) "\/" (v1 "/\" v2)) "\/" v1 = v1
; ( ex v2, v1, v0 being Element of L st not ((v0 "\/" v1) "/\" (v1 "\/" v2)) "/\" v1 = v1 or ( ( for v1, v0 being Element of L holds v0 "/\" (v0 "\/" v1) = v0 ) & ( for v1, v0 being Element of L holds v0 "\/" (v0 "/\" v1) = v0 ) & L is join-commutative & L is meet-commutative & L is meet-associative & L is join-associative ) )
assume A5:
for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" (v1 "\/" v2)) "/\" v1 = v1
; ( ( for v1, v0 being Element of L holds v0 "/\" (v0 "\/" v1) = v0 ) & ( for v1, v0 being Element of L holds v0 "\/" (v0 "/\" v1) = v0 ) & L is join-commutative & L is meet-commutative & L is meet-associative & L is join-associative )
A9:
for v100, v101 being Element of L holds v100 "\/" (v101 "/\" v100) = v100
A13:
for v100, v101 being Element of L holds v100 "/\" (v101 "\/" v100) = v100
A17:
for v101, v100 being Element of L holds (v100 "/\" v101) "\/" v101 = v101
A21:
for v102, v100 being Element of L holds v100 "/\" (v100 "\/" v102) = v100
A25:
for v102, v1, v2, v100 being Element of L holds (v100 "\/" ((v1 "\/" (v100 "\/" v2)) "/\" v102)) "\/" (v1 "\/" (v100 "\/" v2)) = v1 "\/" (v100 "\/" v2)
A33:
for v102, v100 being Element of L holds v100 "\/" (v100 "/\" v102) = v100
A37:
for v102, v1, v2, v100 being Element of L holds (v100 "/\" ((v1 "/\" (v100 "/\" v2)) "\/" v102)) "/\" (v1 "/\" (v100 "/\" v2)) = v1 "/\" (v100 "/\" v2)
A41:
for v101, v100 being Element of L holds (v100 "\/" v101) "/\" v101 = v101
A49:
for v102, v100, v1 being Element of L holds (v100 "/\" ((v1 "/\" v100) "\/" v102)) "/\" (v1 "/\" v100) = v1 "/\" v100
A53:
for v102, v100, v1 being Element of L holds (v100 "\/" ((v1 "\/" v100) "/\" v102)) "\/" (v1 "\/" v100) = v1 "\/" v100
A57:
for v1, v2, v100 being Element of L holds v100 "\/" (v1 "\/" (v100 "\/" v2)) = v1 "\/" (v100 "\/" v2)
A61:
for v100, v1 being Element of L holds v100 "\/" (v1 "\/" v100) = v1 "\/" v100
A65:
for v1, v101 being Element of L holds (v101 "\/" v1) "\/" v101 = v101 "\/" v1
A69:
for v1, v100 being Element of L holds v100 "\/" (v100 "\/" v1) = v100 "\/" v1
A73:
for v1, v101 being Element of L holds (v101 "/\" v1) "/\" v101 = v101 "/\" v1
A77:
for v1, v2, v100 being Element of L holds v100 "/\" (v1 "/\" (v100 "/\" v2)) = v1 "/\" (v100 "/\" v2)
A81:
for v100, v1 being Element of L holds v100 "/\" (v1 "/\" v100) = v1 "/\" v100
A85:
for v1, v2, v101 being Element of L holds (v1 "/\" (v101 "/\" v2)) "\/" v101 = v101 "\/" (v1 "/\" (v101 "/\" v2))
A88:
for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "/\" v2)) "\/" v1 = v1
A91:
for v1, v101 being Element of L holds (v101 "/\" v1) "\/" v101 = v101 "\/" (v101 "/\" v1)
A94:
for v1, v0 being Element of L holds (v0 "/\" v1) "\/" v0 = v0
A97:
for v1, v102, v100 being Element of L holds v100 "/\" ((v100 "\/" v102) "\/" v1) = v100
A101:
for v1, v101 being Element of L holds (v101 "\/" v1) "/\" v101 = v101
A105:
for v103, v102, v100 being Element of L holds (v100 "\/" v103) "\/" (v103 "\/" (v100 "\/" v102)) = v103 "\/" (v100 "\/" v102)
A109:
for v101, v100, v1 being Element of L holds v100 "\/" (v101 "/\" (v1 "/\" v100)) = v100
A113:
for v103, v102, v100 being Element of L holds (v100 "/\" v103) "/\" (v103 "/\" (v100 "/\" v102)) = v103 "/\" (v100 "/\" v102)
A117:
for v1, v102, v101 being Element of L holds ((v101 "/\" v102) "/\" v1) "\/" v101 = v101
A121:
for v2, v1, v101 being Element of L holds ((v101 "\/" v1) "\/" v2) "/\" v101 = v101 "/\" ((v101 "\/" v1) "\/" v2)
A124:
for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "\/" v2) "/\" v0 = v0
A127:
for v1, v100, v2 being Element of L holds v100 "/\" (v1 "/\" (v2 "/\" v100)) = v1 "/\" (v2 "/\" v100)
A131:
for v0, v102, v101 being Element of L holds (v101 "/\" v102) "\/" (v0 "\/" v101) = v0 "\/" v101
A135:
for v1, v102, v101 being Element of L holds (v101 "/\" v102) "\/" (v101 "\/" v1) = v101 "\/" v1
A139:
for v0, v102, v101 being Element of L holds (v101 "\/" v102) "/\" (v0 "/\" v101) = v0 "/\" v101
A143:
for v102, v100 being Element of L holds (v100 "/\" v102) "/\" (v102 "/\" v100) = v102 "/\" v100
A147:
for v100, v1, v102 being Element of L holds (v100 "/\" v102) "/\" ((v102 "/\" v1) "/\" v100) = (v102 "/\" v1) "/\" v100
A151:
for v102, v100 being Element of L holds (v100 "\/" v102) "\/" (v102 "\/" v100) = v102 "\/" v100
A155:
for v100, v101, v2 being Element of L holds (v100 "/\" (v2 "\/" v101)) "/\" (v101 "/\" v100) = v101 "/\" v100
A159:
for v100, v2, v101 being Element of L holds (v100 "/\" (v101 "\/" v2)) "/\" (v101 "/\" v100) = v101 "/\" v100
A163:
for v100, v101, v2 being Element of L holds (v100 "\/" (v2 "/\" v101)) "\/" (v101 "\/" v100) = v101 "\/" v100
A167:
for v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v1 "/\" v0) = v0 "/\" v1
A170:
for v0, v1 being Element of L holds (v1 "/\" v0) "\/" (v0 "/\" v1) = v0 "/\" v1
A173:
for v1, v0 being Element of L holds v0 "/\" v1 = v1 "/\" v0
A182:
for v1, v0 being Element of L holds (v0 "\/" v1) "/\" (v1 "\/" v0) = v0 "\/" v1
A185:
for v0, v1 being Element of L holds (v1 "\/" v0) "\/" (v0 "\/" v1) = (v0 "\/" v1) "\/" (v1 "\/" v0)
A188:
for v0, v1 being Element of L holds v1 "\/" v0 = (v1 "\/" v0) "\/" (v0 "\/" v1)
A191:
for v1, v0 being Element of L holds v0 "\/" v1 = v1 "\/" v0
A200:
for v100, v2, v101 being Element of L holds (v100 "\/" v101) "\/" (v100 "\/" (v101 "\/" v2)) = v101 "\/" (v100 "\/" (v101 "\/" v2))
A203:
for v0, v2, v1 being Element of L holds (v0 "\/" v1) "\/" (v0 "\/" (v1 "\/" v2)) = v0 "\/" (v1 "\/" v2)
A205:
for v1, v2, v0 being Element of L holds (v0 "\/" v1) "\/" ((v0 "\/" v2) "\/" v1) = v1 "\/" (v0 "\/" v2)
A208:
for v102, v100, v1 being Element of L holds (v100 "\/" (v102 "\/" (v1 "/\" v100))) "\/" (v100 "\/" v102) = (v102 "\/" (v1 "/\" v100)) "\/" (v100 "\/" v102)
A211:
for v1, v0, v2 being Element of L holds (v0 "\/" v1) "\/" (v0 "\/" (v1 "\/" (v2 "/\" v0))) = (v1 "\/" (v2 "/\" v0)) "\/" (v0 "\/" v1)
A213:
for v1, v0, v2 being Element of L holds v0 "\/" (v1 "\/" (v2 "/\" v0)) = (v1 "\/" (v2 "/\" v0)) "\/" (v0 "\/" v1)
A215:
for v1, v0, v2 being Element of L holds v0 "\/" (v1 "\/" (v2 "/\" v0)) = v0 "\/" v1
A218:
for v101, v102, v1 being Element of L holds (v1 "\/" v102) "\/" (v101 "\/" v102) = (v1 "\/" v102) "\/" v101
A221:
for v1, v0, v2 being Element of L holds v0 "\/" ((v2 "/\" v0) "\/" v1) = v0 "\/" v1
A224:
for v2, v1, v0 being Element of L holds (v0 "\/" v1) "\/" (v0 "\/" v2) = v1 "\/" (v0 "\/" v2)
A227:
for v102, v1, v101 being Element of L holds (v101 "\/" v1) "\/" (v101 "\/" v102) = (v101 "\/" v1) "\/" v102
A230:
for v1, v2, v0 being Element of L holds v1 "\/" (v0 "\/" v2) = (v0 "\/" v1) "\/" v2
A236:
for v102, v1, v0 being Element of L holds (v1 "\/" v0) "\/" ((v0 "\/" v1) "\/" v102) = (v1 "\/" v0) "\/" v102
A239:
for v0, v2, v1 being Element of L holds (v0 "\/" v1) "\/" (v0 "\/" (v1 "\/" v2)) = (v0 "\/" v1) "\/" v2
A241:
for v0, v2, v1 being Element of L holds v1 "\/" (v0 "\/" (v0 "\/" (v1 "\/" v2))) = (v0 "\/" v1) "\/" v2
A244:
for v1, v2, v0 being Element of L holds v0 "\/" (v1 "\/" (v0 "\/" v2)) = (v1 "\/" v0) "\/" v2
A246:
for v1, v2, v0 being Element of L holds v1 "\/" (v0 "\/" v2) = (v1 "\/" v0) "\/" v2
A257:
for v1, v2, v0 being Element of L holds (v1 "/\" v0) "/\" (v1 "/\" (v0 "/\" v2)) = v1 "/\" (v0 "/\" v2)
A261:
for v102, v100, v1 being Element of L holds (v100 "/\" (v102 "/\" (v1 "\/" v100))) "/\" (v100 "/\" v102) = (v102 "/\" (v1 "\/" v100)) "/\" (v100 "/\" v102)
A264:
for v1, v0, v2 being Element of L holds (v0 "/\" v1) "/\" (v0 "/\" (v1 "/\" (v2 "\/" v0))) = (v1 "/\" (v2 "\/" v0)) "/\" (v0 "/\" v1)
A266:
for v1, v0, v2 being Element of L holds v0 "/\" (v1 "/\" (v2 "\/" v0)) = (v1 "/\" (v2 "\/" v0)) "/\" (v0 "/\" v1)
A268:
for v1, v0, v2 being Element of L holds v0 "/\" (v1 "/\" (v2 "\/" v0)) = v0 "/\" v1
A271:
for v101, v0, v2, v1 being Element of L holds ((v0 "/\" (v1 "\/" v2)) "/\" v101) "/\" (v101 "/\" (v1 "/\" v0)) = v101 "/\" ((v0 "/\" (v1 "\/" v2)) "/\" (v1 "/\" v0))
A274:
for v3, v0, v2, v1 being Element of L holds ((v0 "/\" (v1 "\/" v2)) "/\" v3) "/\" (v3 "/\" (v1 "/\" v0)) = v3 "/\" (v1 "/\" v0)
A277:
for v102, v2, v100 being Element of L holds (v100 "/\" (v102 "/\" (v100 "\/" v2))) "/\" (v100 "/\" v102) = (v102 "/\" (v100 "\/" v2)) "/\" (v100 "/\" v102)
A280:
for v1, v2, v0 being Element of L holds (v0 "/\" v1) "/\" (v0 "/\" (v1 "/\" (v0 "\/" v2))) = (v1 "/\" (v0 "\/" v2)) "/\" (v0 "/\" v1)
A282:
for v1, v2, v0 being Element of L holds v0 "/\" (v1 "/\" (v0 "\/" v2)) = (v1 "/\" (v0 "\/" v2)) "/\" (v0 "/\" v1)
A284:
for v1, v2, v0 being Element of L holds v0 "/\" (v1 "/\" (v0 "\/" v2)) = v0 "/\" v1
A287:
for v101, v1, v102 being Element of L holds (v102 "/\" v1) "/\" (v101 "/\" v102) = (v102 "/\" v1) "/\" v101
A290:
for v1, v0, v2 being Element of L holds v0 "/\" ((v2 "\/" v0) "/\" v1) = v0 "/\" v1
A293:
for v2, v1, v0 being Element of L holds (v0 "/\" v1) "/\" (v1 "/\" v2) = (v1 "/\" v2) "/\" v0
A295:
for v1, v2, v0 being Element of L holds v0 "/\" ((v0 "\/" v2) "/\" v1) = v0 "/\" v1
A299:
for v102, v101, v1 being Element of L holds (v1 "/\" v101) "/\" (v101 "/\" v102) = (v1 "/\" v101) "/\" v102
A303:
for v102, v1, v101 being Element of L holds (v101 "/\" v1) "/\" (v101 "/\" v102) = (v101 "/\" v1) "/\" v102
A307:
for v101, v2, v100, v1 being Element of L holds (v100 "/\" v101) "/\" (v101 "/\" (v100 "/\" v2)) = v101 "/\" (v100 "/\" ((v1 "\/" v100) "/\" v2))
A310:
for v1, v2, v0, v3 being Element of L holds (v0 "/\" v1) "/\" (v0 "/\" v2) = v1 "/\" (v0 "/\" ((v3 "\/" v0) "/\" v2))
A312:
for v1, v2, v0, v3 being Element of L holds (v0 "/\" v1) "/\" v2 = v1 "/\" (v0 "/\" ((v3 "\/" v0) "/\" v2))
A314:
for v2, v1, v0 being Element of L holds (v0 "/\" v1) "/\" v2 = v1 "/\" (v0 "/\" v2)
A316:
for v0, v2, v1 being Element of L holds v1 "/\" (v0 "/\" (v1 "/\" v2)) = (v1 "/\" v2) "/\" v0
A319:
for v1, v2, v0 being Element of L holds v1 "/\" (v0 "/\" v2) = (v0 "/\" v2) "/\" v1
A322:
for v0, v2, v1 being Element of L holds v0 "/\" (v1 "/\" v2) = v2 "/\" (v1 "/\" v0)
A324:
for v0, v3, v2, v1 being Element of L holds ((v1 "\/" v2) "/\" (v0 "/\" v3)) "/\" (v3 "/\" (v1 "/\" v0)) = v3 "/\" (v1 "/\" v0)
A327:
for v2, v3, v1, v0 being Element of L holds (v0 "/\" v2) "/\" (v3 "/\" ((v0 "\/" v1) "/\" (v2 "/\" v3))) = v3 "/\" (v0 "/\" v2)
A330:
for v1, v2, v3, v0 being Element of L holds (v0 "/\" v1) "/\" ((v0 "\/" v3) "/\" (v1 "/\" v2)) = v2 "/\" (v0 "/\" v1)
A333:
for v1, v3, v2, v0 being Element of L holds v1 "/\" (v0 "/\" ((v0 "\/" v2) "/\" (v1 "/\" v3))) = v3 "/\" (v0 "/\" v1)
A336:
for v1, v3, v0 being Element of L holds v0 "/\" (v1 "/\" (v0 "/\" v3)) = v3 "/\" (v1 "/\" v0)
A339:
for v1, v2, v0 being Element of L holds v1 "/\" (v0 "/\" v2) = v2 "/\" (v1 "/\" v0)
for v0, v2, v1 being Element of L holds v0 "/\" (v1 "/\" v2) = (v0 "/\" v1) "/\" v2
hence
( ( for v1, v0 being Element of L holds v0 "/\" (v0 "\/" v1) = v0 ) & ( for v1, v0 being Element of L holds v0 "\/" (v0 "/\" v1) = v0 ) & L is join-commutative & L is meet-commutative & L is meet-associative & L is join-associative )
by A173, A191, A21, A33, A246; verum