let L be non empty LattStr ; ( ( for v2, v0, v5, v4, v3, v1 being Element of L holds (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "/\" v2) "\/" (((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "\/" v2)) = v1 ) implies for v0 being Element of L holds v0 "/\" v0 = v0 )
assume A1:
for v2, v0, v5, v4, v3, v1 being Element of L holds (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "/\" v2) "\/" (((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "\/" v2)) = v1
; for v0 being Element of L holds v0 "/\" v0 = v0
assume
not for v0 being Element of L holds v0 "/\" v0 = v0
; contradiction
then consider C being Element of L such that
A2:
not C "/\" C = C
;
A5:
for v102, v100, v104, v103, v1, v0 being Element of L holds (((v100 "/\" ((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1)))) "\/" (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "/\" (v100 "\/" ((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1)))))) "/\" v102) "\/" (((v100 "/\" (((((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "/\" v103) "\/" (v104 "/\" ((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))))) "\/" ((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))))) "\/" (v1 "/\" (v100 "\/" (((((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "/\" v103) "\/" (v104 "/\" ((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))))) "\/" ((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))))))) "/\" (((v100 "/\" ((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1)))) "\/" (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "/\" (v100 "\/" ((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1)))))) "\/" v102)) = (v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))
A9:
for v103, v100, v105, v104, v0, v5, v4, v3, v1 being Element of L holds (((v100 "/\" v1) "\/" (((((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "/\" ((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))) "\/" (((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "\/" ((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))))) "/\" (v100 "\/" ((((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "/\" ((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))) "\/" (((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "\/" ((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))))))))) "/\" v103) "\/" (((v100 "/\" (((((((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "/\" ((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))) "\/" (((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "\/" ((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))))) "/\" v104) "\/" (v105 "/\" ((((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "/\" ((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))) "\/" (((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "\/" ((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))))))) "\/" ((((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "/\" ((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))) "\/" (((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "\/" ((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))))))) "\/" (((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (v100 "\/" (((((((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "/\" ((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))) "\/" (((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "\/" ((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))))) "/\" v104) "\/" (v105 "/\" ((((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "/\" ((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))) "\/" (((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "\/" ((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))))))) "\/" ((((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "/\" ((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))) "\/" (((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "\/" ((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))))))))) "/\" (((v100 "/\" ((((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "/\" ((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))) "\/" (((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "\/" ((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))))))) "\/" (((((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "/\" ((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))) "\/" (((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "\/" ((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))))) "/\" (v100 "\/" ((((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "/\" ((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))) "\/" (((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "\/" ((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))))))))) "\/" v103)) = (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "/\" ((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))) "\/" (((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "\/" ((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))))
A12:
for v6, v0, v8, v7, v2, v5, v4, v3, v1 being Element of L holds (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" ((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" ((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))) "\/" (((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" ((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))))))))) "/\" v6) "\/" (((v0 "/\" (((((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" ((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))) "\/" (((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" ((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))))) "/\" v7) "\/" (v8 "/\" ((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" ((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))) "\/" (((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" ((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))))))) "\/" ((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" ((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))) "\/" (((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" ((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))))))) "\/" (((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (v0 "\/" (((((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" ((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))) "\/" (((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" ((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))))) "/\" v7) "\/" (v8 "/\" ((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" ((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))) "\/" (((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" ((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))))))) "\/" ((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" ((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))) "\/" (((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" ((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))))))))) "/\" (((v0 "/\" ((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" ((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))) "\/" (((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" ((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))))))) "\/" (((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" ((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))) "\/" (((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" ((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))))) "/\" (v0 "\/" ((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" ((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))) "\/" (((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" ((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))))))))) "\/" v6)) = (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" ((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))) "\/" (((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" ((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))))
A14:
for v6, v0, v8, v7, v2, v5, v4, v3, v1 being Element of L holds (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "/\" v6) "\/" (((v0 "/\" (((((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" ((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))) "\/" (((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" ((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))))) "/\" v7) "\/" (v8 "/\" ((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" ((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))) "\/" (((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" ((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))))))) "\/" ((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" ((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))) "\/" (((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" ((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))))))) "\/" (((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (v0 "\/" (((((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" ((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))) "\/" (((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" ((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))))) "/\" v7) "\/" (v8 "/\" ((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" ((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))) "\/" (((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" ((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))))))) "\/" ((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" ((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))) "\/" (((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" ((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))))))))) "/\" (((v0 "/\" ((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" ((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))) "\/" (((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" ((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))))))) "\/" (((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" ((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))) "\/" (((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" ((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))))) "/\" (v0 "\/" ((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" ((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))) "\/" (((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" ((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))))))))) "\/" v6)) = (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" ((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))) "\/" (((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" ((v2 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v2 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))))
A17:
for v2, v0, v7, v8, v3, v6, v5, v4, v1 being Element of L holds (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "/\" v2) "\/" (((v0 "/\" (((v1 "/\" v7) "\/" (v8 "/\" ((((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "/\" ((v3 "/\" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)) "\/" (v6 "/\" (v1 "\/" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)))) "/\" (v3 "\/" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1))))) "\/" (((v3 "/\" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)) "\/" (v6 "/\" (v1 "\/" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)))) "/\" (v3 "\/" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1)))) "/\" (((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "\/" ((v3 "/\" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)) "\/" (v6 "/\" (v1 "\/" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)))) "/\" (v3 "\/" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1))))))))) "\/" ((((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "/\" ((v3 "/\" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)) "\/" (v6 "/\" (v1 "\/" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)))) "/\" (v3 "\/" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1))))) "\/" (((v3 "/\" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)) "\/" (v6 "/\" (v1 "\/" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)))) "/\" (v3 "\/" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1)))) "/\" (((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "\/" ((v3 "/\" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)) "\/" (v6 "/\" (v1 "\/" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)))) "/\" (v3 "\/" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1))))))))) "\/" (((v3 "/\" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)) "\/" (v6 "/\" (v1 "\/" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)))) "/\" (v3 "\/" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1)))) "/\" (v0 "\/" (((((((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "/\" ((v3 "/\" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)) "\/" (v6 "/\" (v1 "\/" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)))) "/\" (v3 "\/" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1))))) "\/" (((v3 "/\" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)) "\/" (v6 "/\" (v1 "\/" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)))) "/\" (v3 "\/" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1)))) "/\" (((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "\/" ((v3 "/\" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)) "\/" (v6 "/\" (v1 "\/" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)))) "/\" (v3 "\/" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1))))))) "/\" v7) "\/" (v8 "/\" ((((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "/\" ((v3 "/\" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)) "\/" (v6 "/\" (v1 "\/" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)))) "/\" (v3 "\/" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1))))) "\/" (((v3 "/\" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)) "\/" (v6 "/\" (v1 "\/" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)))) "/\" (v3 "\/" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1)))) "/\" (((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "\/" ((v3 "/\" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)) "\/" (v6 "/\" (v1 "\/" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)))) "/\" (v3 "\/" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1))))))))) "\/" ((((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "/\" ((v3 "/\" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)) "\/" (v6 "/\" (v1 "\/" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)))) "/\" (v3 "\/" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1))))) "\/" (((v3 "/\" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)) "\/" (v6 "/\" (v1 "\/" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)))) "/\" (v3 "\/" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1)))) "/\" (((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "\/" ((v3 "/\" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)) "\/" (v6 "/\" (v1 "\/" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)))) "/\" (v3 "\/" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1))))))))))) "/\" (((v0 "/\" ((((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "/\" ((v3 "/\" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)) "\/" (v6 "/\" (v1 "\/" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)))) "/\" (v3 "\/" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1))))) "\/" (((v3 "/\" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)) "\/" (v6 "/\" (v1 "\/" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)))) "/\" (v3 "\/" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1)))) "/\" (((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "\/" ((v3 "/\" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)) "\/" (v6 "/\" (v1 "\/" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)))) "/\" (v3 "\/" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1)))))))) "\/" (((((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "/\" ((v3 "/\" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)) "\/" (v6 "/\" (v1 "\/" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)))) "/\" (v3 "\/" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1))))) "\/" (((v3 "/\" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)) "\/" (v6 "/\" (v1 "\/" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)))) "/\" (v3 "\/" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1)))) "/\" (((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "\/" ((v3 "/\" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)) "\/" (v6 "/\" (v1 "\/" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)))) "/\" (v3 "\/" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1))))))) "/\" (v0 "\/" ((((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "/\" ((v3 "/\" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)) "\/" (v6 "/\" (v1 "\/" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)))) "/\" (v3 "\/" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1))))) "\/" (((v3 "/\" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)) "\/" (v6 "/\" (v1 "\/" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)))) "/\" (v3 "\/" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1)))) "/\" (((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "\/" ((v3 "/\" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)) "\/" (v6 "/\" (v1 "\/" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)))) "/\" (v3 "\/" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1)))))))))) "\/" v2)) = (((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "/\" ((v3 "/\" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)) "\/" (v6 "/\" (v1 "\/" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)))) "/\" (v3 "\/" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1))))) "\/" (((v3 "/\" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)) "\/" (v6 "/\" (v1 "\/" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)))) "/\" (v3 "\/" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1)))) "/\" (((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "\/" ((v3 "/\" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)) "\/" (v6 "/\" (v1 "\/" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)))) "/\" (v3 "\/" (((v1 "/\" v4) "\/" (v5 "/\" v1)) "\/" v1))))))
A20:
for v2, v0, v3, v4, v5, v8, v7, v6, v1 being Element of L holds (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "/\" v2) "\/" (((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" ((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))) "\/" (((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))) "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))))))) "\/" (((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))) "/\" (v0 "\/" (((((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))) "\/" (((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))) "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))))) "/\" v3) "\/" (v4 "/\" ((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))) "\/" (((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))) "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))))))) "\/" ((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))) "\/" (((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))) "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))))))))) "/\" (((v0 "/\" ((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))) "\/" (((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))) "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))))))) "\/" (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))) "\/" (((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))) "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))))) "/\" (v0 "\/" ((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))) "\/" (((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))) "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))))))))) "\/" v2)) = (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))) "\/" (((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))) "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))))
A22:
for v2, v0, v4, v3, v5, v8, v7, v6, v1 being Element of L holds (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "/\" v2) "\/" (((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))) "/\" (v0 "\/" (((((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))) "\/" (((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))) "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))))) "/\" v3) "\/" (v4 "/\" ((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))) "\/" (((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))) "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))))))) "\/" ((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))) "\/" (((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))) "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))))))))) "/\" (((v0 "/\" ((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))) "\/" (((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))) "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))))))) "\/" (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))) "\/" (((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))) "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))))) "/\" (v0 "\/" ((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))) "\/" (((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))) "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))))))))) "\/" v2)) = (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))) "\/" (((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))) "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))))
A24:
for v2, v0, v3, v4, v5, v8, v7, v6, v1 being Element of L holds (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "/\" v2) "\/" (((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" ((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))) "\/" (((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))) "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))))))) "\/" ((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))) "\/" (((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))) "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))))))))) "/\" (((v0 "/\" ((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))) "\/" (((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))) "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))))))) "\/" (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))) "\/" (((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))) "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))))) "/\" (v0 "\/" ((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))) "\/" (((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))) "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))))))))) "\/" v2)) = (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))) "\/" (((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))) "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))))
A26:
for v2, v0, v3, v4, v5, v8, v7, v6, v1 being Element of L holds (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "/\" v2) "\/" (((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" ((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))) "\/" (((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))) "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))))))))) "/\" (((v0 "/\" ((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))) "\/" (((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))) "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))))))) "\/" (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))) "\/" (((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))) "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))))) "/\" (v0 "\/" ((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))) "\/" (((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))) "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))))))))) "\/" v2)) = (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))) "\/" (((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))) "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))))
A28:
for v2, v3, v4, v0, v5, v8, v7, v6, v1 being Element of L holds (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "/\" v2) "\/" (((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v0 "/\" ((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))) "\/" (((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))) "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))))))) "\/" (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))) "\/" (((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))) "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))))) "/\" (v0 "\/" ((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))) "\/" (((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))) "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))))))))) "\/" v2)) = (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))) "\/" (((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))) "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))))
A30:
for v2, v3, v4, v0, v5, v8, v7, v6, v1 being Element of L holds (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "/\" v2) "\/" (((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v0 "/\" v1) "\/" (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))) "\/" (((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))) "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))))) "/\" (v0 "\/" ((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))) "\/" (((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))) "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))))))))) "\/" v2)) = (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))) "\/" (((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))) "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))))
A32:
for v2, v3, v4, v0, v5, v8, v7, v6, v1 being Element of L holds (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "/\" v2) "\/" (((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" ((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))) "\/" (((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))) "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))))))))) "\/" v2)) = (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))) "\/" (((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))) "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))))
A34:
for v2, v3, v4, v0, v5, v8, v7, v6, v1 being Element of L holds (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "/\" v2) "\/" (((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "\/" v2)) = (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))) "\/" (((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))) "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" ((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1))))))
A36:
for v2, v3, v4, v0, v5, v8, v7, v6, v1 being Element of L holds (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "/\" v2) "\/" (((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v5 "/\" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)) "\/" (v8 "/\" (v1 "\/" (((v1 "\/" v6) "/\" (v7 "\/" v1)) "/\" v1)))) "/\" (v5 "\/" (((v1 "/\" v6) "\/" (v7 "/\" v1)) "\/" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "\/" v2)) = v1
A39:
for v102, v101, v105 being Element of L holds (((((v105 "/\" v101) "\/" (v101 "/\" (v105 "\/" v101))) "/\" v101) "\/" (v101 "/\" (((v105 "/\" v101) "\/" (v101 "/\" (v105 "\/" v101))) "\/" v101))) "/\" v102) "\/" (v101 "/\" (((((v105 "/\" v101) "\/" (v101 "/\" (v105 "\/" v101))) "/\" v101) "\/" (v101 "/\" (((v105 "/\" v101) "\/" (v101 "/\" (v105 "\/" v101))) "\/" v101))) "\/" v102)) = v101
A43:
for v103, v100, v105, v104, v102, v0 being Element of L holds (((v100 "/\" v102) "\/" (((((((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "/\" v102) "\/" (v102 "/\" (((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "\/" v102))) "/\" v102) "\/" (v102 "/\" (((((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "/\" v102) "\/" (v102 "/\" (((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "\/" v102))) "\/" v102))) "/\" (v100 "\/" ((((((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "/\" v102) "\/" (v102 "/\" (((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "\/" v102))) "/\" v102) "\/" (v102 "/\" (((((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "/\" v102) "\/" (v102 "/\" (((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "\/" v102))) "\/" v102)))))) "/\" v103) "\/" (((v100 "/\" (((((((((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "/\" v102) "\/" (v102 "/\" (((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "\/" v102))) "/\" v102) "\/" (v102 "/\" (((((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "/\" v102) "\/" (v102 "/\" (((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "\/" v102))) "\/" v102))) "/\" v104) "\/" (v105 "/\" ((((((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "/\" v102) "\/" (v102 "/\" (((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "\/" v102))) "/\" v102) "\/" (v102 "/\" (((((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "/\" v102) "\/" (v102 "/\" (((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "\/" v102))) "\/" v102))))) "\/" ((((((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "/\" v102) "\/" (v102 "/\" (((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "\/" v102))) "/\" v102) "\/" (v102 "/\" (((((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "/\" v102) "\/" (v102 "/\" (((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "\/" v102))) "\/" v102))))) "\/" (v102 "/\" (v100 "\/" (((((((((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "/\" v102) "\/" (v102 "/\" (((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "\/" v102))) "/\" v102) "\/" (v102 "/\" (((((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "/\" v102) "\/" (v102 "/\" (((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "\/" v102))) "\/" v102))) "/\" v104) "\/" (v105 "/\" ((((((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "/\" v102) "\/" (v102 "/\" (((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "\/" v102))) "/\" v102) "\/" (v102 "/\" (((((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "/\" v102) "\/" (v102 "/\" (((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "\/" v102))) "\/" v102))))) "\/" ((((((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "/\" v102) "\/" (v102 "/\" (((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "\/" v102))) "/\" v102) "\/" (v102 "/\" (((((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "/\" v102) "\/" (v102 "/\" (((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "\/" v102))) "\/" v102))))))) "/\" (((v100 "/\" ((((((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "/\" v102) "\/" (v102 "/\" (((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "\/" v102))) "/\" v102) "\/" (v102 "/\" (((((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "/\" v102) "\/" (v102 "/\" (((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "\/" v102))) "\/" v102)))) "\/" (((((((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "/\" v102) "\/" (v102 "/\" (((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "\/" v102))) "/\" v102) "\/" (v102 "/\" (((((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "/\" v102) "\/" (v102 "/\" (((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "\/" v102))) "\/" v102))) "/\" (v100 "\/" ((((((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "/\" v102) "\/" (v102 "/\" (((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "\/" v102))) "/\" v102) "\/" (v102 "/\" (((((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "/\" v102) "\/" (v102 "/\" (((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "\/" v102))) "\/" v102)))))) "\/" v103)) = (((((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "/\" v102) "\/" (v102 "/\" (((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "\/" v102))) "/\" v102) "\/" (v102 "/\" (((((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "/\" v102) "\/" (v102 "/\" (((v0 "/\" v102) "\/" (v102 "/\" (v0 "\/" v102))) "\/" v102))) "\/" v102))
A46:
for v3, v0, v5, v4, v1, v2 being Element of L holds (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" ((((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" v1))) "\/" v1)))))) "/\" v3) "\/" (((v0 "/\" (((((((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" v1))) "\/" v1))) "/\" v4) "\/" (v5 "/\" ((((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" v1))) "\/" v1))))) "\/" ((((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" v1))) "\/" v1))))) "\/" (v1 "/\" (v0 "\/" (((((((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" v1))) "\/" v1))) "/\" v4) "\/" (v5 "/\" ((((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" v1))) "\/" v1))))) "\/" ((((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" v1))) "\/" v1))))))) "/\" (((v0 "/\" ((((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" v1))) "\/" v1)))) "\/" (((((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" v1))) "\/" v1))) "/\" (v0 "\/" ((((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" v1))) "\/" v1)))))) "\/" v3)) = (((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" v1))) "\/" v1))
A48:
for v3, v0, v5, v4, v1, v2 being Element of L holds (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "/\" v3) "\/" (((v0 "/\" (((((((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" v1))) "\/" v1))) "/\" v4) "\/" (v5 "/\" ((((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" v1))) "\/" v1))))) "\/" ((((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" v1))) "\/" v1))))) "\/" (v1 "/\" (v0 "\/" (((((((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" v1))) "\/" v1))) "/\" v4) "\/" (v5 "/\" ((((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" v1))) "\/" v1))))) "\/" ((((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" v1))) "\/" v1))))))) "/\" (((v0 "/\" ((((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" v1))) "\/" v1)))) "\/" (((((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" v1))) "\/" v1))) "/\" (v0 "\/" ((((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" v1))) "\/" v1)))))) "\/" v3)) = (((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v2 "/\" v1) "\/" (v1 "/\" (v2 "\/" v1))) "\/" v1))) "\/" v1))
A51:
for v2, v0, v4, v5, v1, v3 being Element of L holds (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "/\" v2) "\/" (((v0 "/\" (((v1 "/\" v4) "\/" (v5 "/\" ((((((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "\/" v1))) "\/" v1))))) "\/" ((((((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "\/" v1))) "\/" v1))))) "\/" (v1 "/\" (v0 "\/" (((((((((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "\/" v1))) "\/" v1))) "/\" v4) "\/" (v5 "/\" ((((((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "\/" v1))) "\/" v1))))) "\/" ((((((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "\/" v1))) "\/" v1))))))) "/\" (((v0 "/\" ((((((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "\/" v1))) "\/" v1)))) "\/" (((((((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "\/" v1))) "\/" v1))) "/\" (v0 "\/" ((((((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "\/" v1))) "\/" v1)))))) "\/" v2)) = (((((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v3 "/\" v1) "\/" (v1 "/\" (v3 "\/" v1))) "\/" v1))) "\/" v1))
A54:
for v2, v0, v5, v4, v3, v1 being Element of L holds (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "/\" v2) "\/" (((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" ((((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "\/" v1))))) "\/" (v1 "/\" (v0 "\/" (((((((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "\/" v1))) "/\" v3) "\/" (v4 "/\" ((((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "\/" v1))))) "\/" ((((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "\/" v1))))))) "/\" (((v0 "/\" ((((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "\/" v1)))) "\/" (((((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "\/" v1))) "/\" (v0 "\/" ((((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "\/" v1)))))) "\/" v2)) = (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "\/" v1))
A56:
for v2, v0, v4, v3, v1, v5 being Element of L holds (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "/\" v2) "\/" (((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (v1 "/\" (v0 "\/" (((((((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "\/" v1))) "/\" v3) "\/" (v4 "/\" ((((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "\/" v1))))) "\/" ((((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "\/" v1))))))) "/\" (((v0 "/\" ((((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "\/" v1)))) "\/" (((((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "\/" v1))) "/\" (v0 "\/" ((((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "\/" v1)))))) "\/" v2)) = (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "\/" v1))
A58:
for v2, v0, v3, v4, v1, v5 being Element of L holds (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "/\" v2) "\/" (((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (v1 "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" ((((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "\/" v1))))) "\/" ((((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "\/" v1))))))) "/\" (((v0 "/\" ((((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "\/" v1)))) "\/" (((((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "\/" v1))) "/\" (v0 "\/" ((((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "\/" v1)))))) "\/" v2)) = (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "\/" v1))
A60:
for v2, v0, v5, v4, v3, v1 being Element of L holds (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "/\" v2) "\/" (((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (v1 "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" ((((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "\/" v1))))))) "/\" (((v0 "/\" ((((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "\/" v1)))) "\/" (((((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "\/" v1))) "/\" (v0 "\/" ((((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "\/" v1)))))) "\/" v2)) = (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "\/" v1))
A62:
for v5, v2, v0, v4, v3, v1 being Element of L holds (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "/\" v2) "\/" (((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (v1 "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v0 "/\" ((((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "\/" v1)))) "\/" (((((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "\/" v1))) "/\" (v0 "\/" ((((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "\/" v1)))))) "\/" v2)) = (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "\/" v1))
A64:
for v5, v2, v0, v4, v3, v1 being Element of L holds (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "/\" v2) "\/" (((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (v1 "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v0 "/\" v1) "\/" (((((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "\/" v1))) "/\" (v0 "\/" ((((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "\/" v1)))))) "\/" v2)) = (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "\/" v1))
A66:
for v5, v2, v0, v4, v3, v1 being Element of L holds (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "/\" v2) "\/" (((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (v1 "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" ((((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "\/" v1)))))) "\/" v2)) = (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "\/" v1))
A68:
for v5, v2, v0, v4, v3, v1 being Element of L holds (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "/\" v2) "\/" (((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (v1 "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "\/" v2)) = (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "/\" v1) "\/" (v1 "/\" (((((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "/\" v1) "\/" (v1 "/\" (((v5 "/\" v1) "\/" (v1 "/\" (v5 "\/" v1))) "\/" v1))) "\/" v1))
A70:
for v2, v0, v4, v3, v1 being Element of L holds (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "/\" v2) "\/" (((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (v1 "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "\/" v2)) = v1
A73:
for v102, v103, v104, v100, v108, v107, v106, v101 being Element of L holds (((v100 "/\" v101) "\/" (v101 "/\" (v100 "\/" v101))) "/\" v102) "\/" (((v100 "/\" (((v101 "/\" v103) "\/" (v104 "/\" v101)) "\/" v101)) "\/" (((v101 "/\" (((v101 "\/" v106) "/\" (v107 "\/" v101)) "/\" v101)) "\/" (v108 "/\" (v101 "\/" (((v101 "\/" v106) "/\" (v107 "\/" v101)) "/\" v101)))) "/\" (v100 "\/" (((v101 "/\" v103) "\/" (v104 "/\" v101)) "\/" v101)))) "/\" (((v100 "/\" v101) "\/" (v101 "/\" (v100 "\/" v101))) "\/" v102)) = v101
A77:
for v102, v101, v0 being Element of L holds (v101 "/\" v102) "\/" (v101 "/\" (((((((v0 "/\" v101) "\/" (v101 "/\" (v0 "\/" v101))) "/\" v101) "\/" (v101 "/\" (((v0 "/\" v101) "\/" (v101 "/\" (v0 "\/" v101))) "\/" v101))) "/\" v101) "\/" (v101 "/\" (((((v0 "/\" v101) "\/" (v101 "/\" (v0 "\/" v101))) "/\" v101) "\/" (v101 "/\" (((v0 "/\" v101) "\/" (v101 "/\" (v0 "\/" v101))) "\/" v101))) "\/" v101))) "\/" v102)) = v101
A80:
for v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" (v0 "\/" v1)) = v0
A83:
for v103, v102, v101 being Element of L holds (((v102 "/\" ((v101 "/\" v102) "\/" (v102 "/\" (v101 "\/" v102)))) "\/" (((v101 "/\" v102) "\/" (v102 "/\" (v101 "\/" v102))) "/\" (v102 "\/" ((v101 "/\" v102) "\/" (v102 "/\" (v101 "\/" v102)))))) "/\" v103) "\/" (v102 "/\" (((v102 "/\" ((v101 "/\" v102) "\/" (v102 "/\" (v101 "\/" v102)))) "\/" (((v101 "/\" v102) "\/" (v102 "/\" (v101 "\/" v102))) "/\" (v102 "\/" ((v101 "/\" v102) "\/" (v102 "/\" (v101 "\/" v102)))))) "\/" v103)) = (v101 "/\" v102) "\/" (v102 "/\" (v101 "\/" v102))
A87:
for v102, v104, v103, v0, v4, v3, v1 being Element of L holds (v1 "/\" v102) "\/" (((((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "/\" (((((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (v1 "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" v103) "\/" (v104 "/\" ((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (v1 "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))))) "\/" ((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (v1 "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))))) "\/" (((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (v1 "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "\/" (((((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (v1 "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" v103) "\/" (v104 "/\" ((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (v1 "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))))) "\/" ((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (v1 "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))))))) "/\" (((((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "/\" ((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (v1 "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))) "\/" (((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (v1 "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "\/" ((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (v1 "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1))))))) "\/" v102)) = (v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (v1 "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))
A90:
for v1, v2, v4, v3, v0 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" (((((v2 "/\" v0) "\/" (v0 "/\" (v2 "\/" v0))) "/\" ((v2 "/\" (((v0 "/\" v3) "\/" (v4 "/\" v0)) "\/" v0)) "\/" (v0 "/\" (v2 "\/" (((v0 "/\" v3) "\/" (v4 "/\" v0)) "\/" v0))))) "\/" (((v2 "/\" (((v0 "/\" v3) "\/" (v4 "/\" v0)) "\/" v0)) "\/" (v0 "/\" (v2 "\/" (((v0 "/\" v3) "\/" (v4 "/\" v0)) "\/" v0)))) "/\" (((v2 "/\" v0) "\/" (v0 "/\" (v2 "\/" v0))) "\/" ((v2 "/\" (((v0 "/\" v3) "\/" (v4 "/\" v0)) "\/" v0)) "\/" (v0 "/\" (v2 "\/" (((v0 "/\" v3) "\/" (v4 "/\" v0)) "\/" v0))))))) "\/" v1)) = (v2 "/\" (((v0 "/\" v3) "\/" (v4 "/\" v0)) "\/" v0)) "\/" (v0 "/\" (v2 "\/" (((v0 "/\" v3) "\/" (v4 "/\" v0)) "\/" v0)))
A92:
for v1, v2, v4, v3, v0 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" (v0 "\/" v1)) = (v2 "/\" (((v0 "/\" v3) "\/" (v4 "/\" v0)) "\/" v0)) "\/" (v0 "/\" (v2 "\/" (((v0 "/\" v3) "\/" (v4 "/\" v0)) "\/" v0)))
A94:
for v2, v4, v3, v0 being Element of L holds v0 = (v2 "/\" (((v0 "/\" v3) "\/" (v4 "/\" v0)) "\/" v0)) "\/" (v0 "/\" (v2 "\/" (((v0 "/\" v3) "\/" (v4 "/\" v0)) "\/" v0)))
A100:
for v3, v4, v0, v7, v6, v5, v1 being Element of L holds v1 = (v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v5) "/\" (v6 "\/" v1)) "/\" v1)) "\/" (v7 "/\" (v1 "\/" (((v1 "\/" v5) "/\" (v6 "\/" v1)) "/\" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))
A106:
for v6, v5, v4, v1 being Element of L holds v1 = (v1 "/\" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)) "\/" (v6 "/\" (v1 "\/" (((v1 "\/" v4) "/\" (v5 "\/" v1)) "/\" v1)))
A111:
for v101, v1 being Element of L holds (v1 "/\" v101) "\/" (v101 "/\" (v1 "\/" v101)) = v101
A115:
for v2, v1, v100 being Element of L holds v100 = ((v100 "\/" v1) "/\" (v2 "\/" v100)) "/\" v100
A119:
for v3, v2, v1, v0 being Element of L holds (v0 "/\" v0) "\/" (v3 "/\" (v0 "\/" (((v0 "\/" v1) "/\" (v2 "\/" v0)) "/\" v0))) = v0
A122:
for v0, v1 being Element of L holds (v0 "/\" v0) "\/" (v1 "/\" (v0 "\/" v0)) = v0
A125:
for v103, v102, v101 being Element of L holds ((v101 "/\" v102) "\/" (v103 "/\" v101)) "\/" v101 = v101
A129:
for v101, v100 being Element of L holds ((v100 "\/" v101) "/\" v100) "/\" v100 = v100
A133:
for v1, v0 being Element of L holds (v0 "/\" (v0 "/\" v1)) "/\" (v0 "/\" v1) = v0 "/\" v1
A136:
for v2, v1, v101 being Element of L holds (((v101 "\/" v1) "/\" (v2 "\/" v101)) "/\" v101) "/\" (((v101 "\/" v1) "/\" (v2 "\/" v101)) "/\" v101) = ((v101 "\/" v1) "/\" (v2 "\/" v101)) "/\" v101
A139:
for v2, v1, v0 being Element of L holds v0 "/\" (((v0 "\/" v1) "/\" (v2 "\/" v0)) "/\" v0) = ((v0 "\/" v1) "/\" (v2 "\/" v0)) "/\" v0
A141:
for v2, v1, v0 being Element of L holds v0 "/\" v0 = ((v0 "\/" v1) "/\" (v2 "\/" v0)) "/\" v0
for v0 being Element of L holds v0 "/\" v0 = v0
hence
contradiction
by A2; verum