proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = (v0 "\/" v1) "/\" (v0 "\/" (v1 "/\" v2)) by A4;
hence (v0 "\/" v1) "/\" (v0 "\/" (v1 "/\" v2)) = v0 "\/" (v1 "/\" v2) by A9; :: thesis:

end;

assume A12: for v2, v1, v0 being Element of L holds (((v0 "/\" v1) "\/" v2) "/\" v1) "\/" (v2 "/\" v0) = (((v0 "\/" v1) "/\" v2) "\/" v1) "/\" (v2 "\/" v0) ; :: thesis:
A14: for v2, v1, v0 being Element of L holds (v1 "/\" ((v0 "/\" v1) "\/" v2)) "\/" (v2 "/\" v0) = (((v0 "\/" v1) "/\" v2) "\/" v1) "/\" (v2 "\/" v0)

proof

let v2, v1, v0 be Element of L; :: thesis:
((v0 "/\" v1) "\/" v2) "/\" v1 = v1 "/\" ((v0 "/\" v1) "\/" v2) by A4;
hence (v1 "/\" ((v0 "/\" v1) "\/" v2)) "\/" (v2 "/\" v0) = (((v0 "\/" v1) "/\" v2) "\/" v1) "/\" (v2 "\/" v0) by A12; :: thesis:

end;

A17: for v2, v0, v1 being Element of L holds (v2 "/\" v1) "\/" (v0 "/\" ((v1 "/\" v0) "\/" v2)) = (((v1 "\/" v0) "/\" v2) "\/" v0) "/\" (v2 "\/" v1)

proof

let v2, v0, v1 be Element of L; :: thesis:
(v0 "/\" ((v1 "/\" v0) "\/" v2)) "\/" (v2 "/\" v1) = (v2 "/\" v1) "\/" (v0 "/\" ((v1 "/\" v0) "\/" v2)) by A8;
hence (v2 "/\" v1) "\/" (v0 "/\" ((v1 "/\" v0) "\/" v2)) = (((v1 "\/" v0) "/\" v2) "\/" v0) "/\" (v2 "\/" v1) by A14; :: thesis:

end;

A20: for v0, v2, v1 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" ((v1 "/\" v2) "\/" v0)) = (v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v0 "\/" v1)

proof

let v0, v2, v1 be Element of L; :: thesis:
((v1 "\/" v2) "/\" v0) "\/" v2 = v2 "\/" ((v1 "\/" v2) "/\" v0) by A8;
hence (v0 "/\" v1) "\/" (v2 "/\" ((v1 "/\" v2) "\/" v0)) = (v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v0 "\/" v1) by A17; :: thesis:

end;

A23: for v0, v2, v1 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" (v1 "\/" v2)) = v0 "/\" (v1 "\/" v2)

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = (v0 "/\" v1) "\/" (v0 "/\" (v1 "\/" v2)) by A8;
hence (v0 "/\" v1) "\/" (v0 "/\" (v1 "\/" v2)) = v0 "/\" (v1 "\/" v2) by A5; :: thesis:

end;

A26: for v102, v101 being Element of L holds v101 "/\" v102 = v101 "/\" (v101 "/\" v102)

proof

let v102, v101 be Element of L; :: thesis:
v101 "/\" v101 = v101 by A2;
hence v101 "/\" v102 = v101 "/\" (v101 "/\" v102) by A3; :: thesis:

end;

A31: for v102, v100 being Element of L holds (v100 "/\" v102) "/\" v102 = v100 "/\" v102

proof

let v102, v100 be Element of L; :: thesis:
v102 "/\" v102 = v102 by A2;
hence (v100 "/\" v102) "/\" v102 = v100 "/\" v102 by A3; :: thesis:

end;

A34: for v1, v0 being Element of L holds v1 "/\" (v0 "/\" v1) = v0 "/\" v1

proof

let v1, v0 be Element of L; :: thesis:
(v0 "/\" v1) "/\" v1 = v1 "/\" (v0 "/\" v1) by A4;
hence v1 "/\" (v0 "/\" v1) = v0 "/\" v1 by A31; :: thesis:

end;

A37: for v2, v0, v1 being Element of L holds (v1 "/\" v0) "/\" v2 = v0 "/\" (v1 "/\" v2)

proof

let v2, v0, v1 be Element of L; :: thesis:
v0 "/\" v1 = v1 "/\" v0 by A4;
hence (v1 "/\" v0) "/\" v2 = v0 "/\" (v1 "/\" v2) by A3; :: thesis:

end;

A40: for v0, v2, v1 being Element of L holds v0 "/\" (v1 "/\" v2) = v1 "/\" (v0 "/\" v2)

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "/\" v1) "/\" v2 = v0 "/\" (v1 "/\" v2) by A3;
hence v0 "/\" (v1 "/\" v2) = v1 "/\" (v0 "/\" v2) by A37; :: thesis:

end;

A43: for v102, v101 being Element of L holds v101 "\/" v102 = v101 "\/" (v101 "\/" v102)

proof

let v102, v101 be Element of L; :: thesis:
v101 "\/" v101 = v101 by A6;
hence v101 "\/" v102 = v101 "\/" (v101 "\/" v102) by A7; :: thesis:

end;

A48: for v102, v100 being Element of L holds (v100 "\/" v102) "\/" v102 = v100 "\/" v102

proof

let v102, v100 be Element of L; :: thesis:
v102 "\/" v102 = v102 by A6;
hence (v100 "\/" v102) "\/" v102 = v100 "\/" v102 by A7; :: thesis:

end;

A51: for v1, v0 being Element of L holds v1 "\/" (v0 "\/" v1) = v0 "\/" v1

proof

let v1, v0 be Element of L; :: thesis:
(v0 "\/" v1) "\/" v1 = v1 "\/" (v0 "\/" v1) by A8;
hence v1 "\/" (v0 "\/" v1) = v0 "\/" v1 by A48; :: thesis:

end;

A54: for v2, v0, v1 being Element of L holds (v1 "\/" v0) "\/" v2 = v0 "\/" (v1 "\/" v2)

proof

let v2, v0, v1 be Element of L; :: thesis:
v0 "\/" v1 = v1 "\/" v0 by A8;
hence (v1 "\/" v0) "\/" v2 = v0 "\/" (v1 "\/" v2) by A7; :: thesis:

end;

A57: for v0, v2, v1 being Element of L holds v0 "\/" (v1 "\/" v2) = v1 "\/" (v0 "\/" v2)

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) by A7;
hence v0 "\/" (v1 "\/" v2) = v1 "\/" (v0 "\/" v2) by A54; :: thesis:

end;

A60: for v102, v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" v102 = (v0 "\/" v1) "/\" ((v0 "\/" (v1 "/\" v2)) "/\" v102)

proof

let v102, v0, v2, v1 be Element of L; :: thesis:
(v0 "\/" v1) "/\" (v0 "\/" (v1 "/\" v2)) = v0 "\/" (v1 "/\" v2) by A11;
hence (v0 "\/" (v1 "/\" v2)) "/\" v102 = (v0 "\/" v1) "/\" ((v0 "\/" (v1 "/\" v2)) "/\" v102) by A3; :: thesis:

end;

A65: for v100, v0, v102, v1 being Element of L holds (v100 "\/" (v0 "/\" v1)) "/\" (v100 "\/" (v0 "/\" (v1 "/\" v102))) = v100 "\/" ((v0 "/\" v1) "/\" v102)

proof

let v100, v0, v102, v1 be Element of L; :: thesis:
(v0 "/\" v1) "/\" v102 = v0 "/\" (v1 "/\" v102) by A3;
hence (v100 "\/" (v0 "/\" v1)) "/\" (v100 "\/" (v0 "/\" (v1 "/\" v102))) = v100 "\/" ((v0 "/\" v1) "/\" v102) by A11; :: thesis:

end;

A68: for v0, v1, v3, v2 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" (v1 "/\" (v2 "/\" v3))) = v0 "\/" (v1 "/\" (v2 "/\" v3))

proof

let v0, v1, v3, v2 be Element of L; :: thesis:
(v1 "/\" v2) "/\" v3 = v1 "/\" (v2 "/\" v3) by A3;
hence (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" (v1 "/\" (v2 "/\" v3))) = v0 "\/" (v1 "/\" (v2 "/\" v3)) by A65; :: thesis:

end;

A71: for v102, v101 being Element of L holds v101 "/\" (v101 "\/" (v101 "/\" v102)) = v101 "\/" (v101 "/\" v102)

proof

let v102, v101 be Element of L; :: thesis:
v101 "\/" v101 = v101 by A6;
hence v101 "/\" (v101 "\/" (v101 "/\" v102)) = v101 "\/" (v101 "/\" v102) by A11; :: thesis:

end;

A75: for v102, v101 being Element of L holds ((v101 "/\" v102) "\/" v101) "/\" (v101 "/\" v102) = (v101 "/\" v102) "\/" (v101 "/\" v102)

proof

let v102, v101 be Element of L; :: thesis:
(v101 "/\" v102) "\/" (v101 "/\" v102) = v101 "/\" v102 by A6;
hence ((v101 "/\" v102) "\/" v101) "/\" (v101 "/\" v102) = (v101 "/\" v102) "\/" (v101 "/\" v102) by A11; :: thesis:

end;

A78: for v1, v0 being Element of L holds (v0 "\/" (v0 "/\" v1)) "/\" (v0 "/\" v1) = (v0 "/\" v1) "\/" (v0 "/\" v1)

proof

let v1, v0 be Element of L; :: thesis:
(v0 "/\" v1) "\/" v0 = v0 "\/" (v0 "/\" v1) by A8;
hence (v0 "\/" (v0 "/\" v1)) "/\" (v0 "/\" v1) = (v0 "/\" v1) "\/" (v0 "/\" v1) by A75; :: thesis:

end;

A80: for v1, v0 being Element of L holds (v0 "/\" v1) "/\" (v0 "\/" (v0 "/\" v1)) = (v0 "/\" v1) "\/" (v0 "/\" v1)

proof

let v1, v0 be Element of L; :: thesis:
(v0 "\/" (v0 "/\" v1)) "/\" (v0 "/\" v1) = (v0 "/\" v1) "/\" (v0 "\/" (v0 "/\" v1)) by A4;
hence (v0 "/\" v1) "/\" (v0 "\/" (v0 "/\" v1)) = (v0 "/\" v1) "\/" (v0 "/\" v1) by A78; :: thesis:

end;

A82: for v1, v0 being Element of L holds v0 "/\" (v1 "/\" (v0 "\/" (v0 "/\" v1))) = (v0 "/\" v1) "\/" (v0 "/\" v1)

proof

let v1, v0 be Element of L; :: thesis:
(v0 "/\" v1) "/\" (v0 "\/" (v0 "/\" v1)) = v0 "/\" (v1 "/\" (v0 "\/" (v0 "/\" v1))) by A3;
hence v0 "/\" (v1 "/\" (v0 "\/" (v0 "/\" v1))) = (v0 "/\" v1) "\/" (v0 "/\" v1) by A80; :: thesis:

end;

A84: for v1, v0 being Element of L holds v0 "/\" (v1 "/\" (v0 "\/" (v0 "/\" v1))) = v0 "/\" v1

proof

let v1, v0 be Element of L; :: thesis:
(v0 "/\" v1) "\/" (v0 "/\" v1) = v0 "/\" v1 by A6;
hence v0 "/\" (v1 "/\" (v0 "\/" (v0 "/\" v1))) = v0 "/\" v1 by A82; :: thesis:

end;

A86: for v0, v2, v1 being Element of L holds (v1 "\/" v0) "/\" (v0 "\/" (v1 "/\" v2)) = v0 "\/" (v1 "/\" v2)

proof

let v0, v2, v1 be Element of L; :: thesis:
v0 "\/" v1 = v1 "\/" v0 by A8;
hence (v1 "\/" v0) "/\" (v0 "\/" (v1 "/\" v2)) = v0 "\/" (v1 "/\" v2) by A11; :: thesis:

end;

A90: for v102, v101 being Element of L holds v101 "\/" (v102 "/\" ((v101 "/\" v102) "\/" v101)) = (v102 "\/" ((v101 "\/" v102) "/\" v101)) "/\" (v101 "\/" v101)

proof

let v102, v101 be Element of L; :: thesis:
v101 "/\" v101 = v101 by A2;
hence v101 "\/" (v102 "/\" ((v101 "/\" v102) "\/" v101)) = (v102 "\/" ((v101 "\/" v102) "/\" v101)) "/\" (v101 "\/" v101) by A20; :: thesis:

end;

A93: for v1, v0 being Element of L holds v0 "\/" (v1 "/\" (v0 "\/" (v0 "/\" v1))) = (v1 "\/" ((v0 "\/" v1) "/\" v0)) "/\" (v0 "\/" v0)

proof

let v1, v0 be Element of L; :: thesis:
(v0 "/\" v1) "\/" v0 = v0 "\/" (v0 "/\" v1) by A8;
hence v0 "\/" (v1 "/\" (v0 "\/" (v0 "/\" v1))) = (v1 "\/" ((v0 "\/" v1) "/\" v0)) "/\" (v0 "\/" v0) by A90; :: thesis:

end;

A95: for v1, v0 being Element of L holds v0 "\/" (v1 "/\" (v0 "\/" (v0 "/\" v1))) = (v1 "\/" (v0 "/\" (v0 "\/" v1))) "/\" (v0 "\/" v0)

proof

let v1, v0 be Element of L; :: thesis:
(v0 "\/" v1) "/\" v0 = v0 "/\" (v0 "\/" v1) by A4;
hence v0 "\/" (v1 "/\" (v0 "\/" (v0 "/\" v1))) = (v1 "\/" (v0 "/\" (v0 "\/" v1))) "/\" (v0 "\/" v0) by A93; :: thesis:

end;

A97: for v1, v0 being Element of L holds v0 "\/" (v1 "/\" (v0 "\/" (v0 "/\" v1))) = (v1 "\/" (v0 "/\" (v0 "\/" v1))) "/\" v0

proof

let v1, v0 be Element of L; :: thesis:
v0 "\/" v0 = v0 by A6;
hence v0 "\/" (v1 "/\" (v0 "\/" (v0 "/\" v1))) = (v1 "\/" (v0 "/\" (v0 "\/" v1))) "/\" v0 by A95; :: thesis:

end;

A99: for v1, v0 being Element of L holds v0 "\/" (v1 "/\" (v0 "\/" (v0 "/\" v1))) = v0 "/\" (v1 "\/" (v0 "/\" (v0 "\/" v1)))

proof

let v1, v0 be Element of L; :: thesis:
(v1 "\/" (v0 "/\" (v0 "\/" v1))) "/\" v0 = v0 "/\" (v1 "\/" (v0 "/\" (v0 "\/" v1))) by A4;
hence v0 "\/" (v1 "/\" (v0 "\/" (v0 "/\" v1))) = v0 "/\" (v1 "\/" (v0 "/\" (v0 "\/" v1))) by A97; :: thesis:

end;

A101: for v0, v2, v1 being Element of L holds (v1 "/\" v0) "\/" (v2 "/\" ((v1 "/\" v2) "\/" v0)) = (v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v0 "\/" v1)

proof

let v0, v2, v1 be Element of L; :: thesis:
v0 "/\" v1 = v1 "/\" v0 by A4;
hence (v1 "/\" v0) "\/" (v2 "/\" ((v1 "/\" v2) "\/" v0)) = (v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v0 "\/" v1) by A20; :: thesis:

end;

A104: for v0, v1, v2 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" ((v2 "/\" v1) "\/" v0)) = (v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v0 "\/" v1)

proof

let v0, v1, v2 be Element of L; :: thesis:
v1 "/\" v2 = v2 "/\" v1 by A4;
hence (v0 "/\" v1) "\/" (v2 "/\" ((v2 "/\" v1) "\/" v0)) = (v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v0 "\/" v1) by A20; :: thesis:

end;

A107: for v101, v1, v0 being Element of L holds ((v0 "/\" v1) "\/" v101) "/\" ((v101 "\/" ((v1 "\/" v101) "/\" v0)) "/\" (v0 "\/" v1)) = (v0 "/\" v1) "\/" (v101 "/\" ((v1 "/\" v101) "\/" v0))

proof

let v101, v1, v0 be Element of L; :: thesis:
(v0 "/\" v1) "\/" (v101 "/\" ((v1 "/\" v101) "\/" v0)) = (v101 "\/" ((v1 "\/" v101) "/\" v0)) "/\" (v0 "\/" v1) by A20;
hence ((v0 "/\" v1) "\/" v101) "/\" ((v101 "\/" ((v1 "\/" v101) "/\" v0)) "/\" (v0 "\/" v1)) = (v0 "/\" v1) "\/" (v101 "/\" ((v1 "/\" v101) "\/" v0)) by A11; :: thesis:

end;

A110: for v2, v1, v0 being Element of L holds ((v0 "/\" v1) "\/" v2) "/\" ((v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v0 "\/" v1)) = (v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v0 "\/" v1)

proof

let v2, v1, v0 be Element of L; :: thesis:
(v0 "/\" v1) "\/" (v2 "/\" ((v1 "/\" v2) "\/" v0)) = (v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v0 "\/" v1) by A20;
hence ((v0 "/\" v1) "\/" v2) "/\" ((v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v0 "\/" v1)) = (v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v0 "\/" v1) by A107; :: thesis:

end;

A113: for v102, v101 being Element of L holds v101 "\/" (v101 "/\" (v101 "\/" v102)) = v101 "/\" (v101 "\/" v102)

proof

let v102, v101 be Element of L; :: thesis:
v101 "/\" v101 = v101 by A2;
hence v101 "\/" (v101 "/\" (v101 "\/" v102)) = v101 "/\" (v101 "\/" v102) by A23; :: thesis:

end;

A117: for v102, v101 being Element of L holds ((v101 "\/" v102) "/\" v101) "\/" (v101 "\/" v102) = (v101 "\/" v102) "/\" (v101 "\/" v102)

proof

let v102, v101 be Element of L; :: thesis:
(v101 "\/" v102) "/\" (v101 "\/" v102) = v101 "\/" v102 by A2;
hence ((v101 "\/" v102) "/\" v101) "\/" (v101 "\/" v102) = (v101 "\/" v102) "/\" (v101 "\/" v102) by A23; :: thesis:

end;

A120: for v1, v0 being Element of L holds (v0 "/\" (v0 "\/" v1)) "\/" (v0 "\/" v1) = (v0 "\/" v1) "/\" (v0 "\/" v1)

proof

let v1, v0 be Element of L; :: thesis:
(v0 "\/" v1) "/\" v0 = v0 "/\" (v0 "\/" v1) by A4;
hence (v0 "/\" (v0 "\/" v1)) "\/" (v0 "\/" v1) = (v0 "\/" v1) "/\" (v0 "\/" v1) by A117; :: thesis:

end;

A122: for v1, v0 being Element of L holds (v0 "\/" v1) "\/" (v0 "/\" (v0 "\/" v1)) = (v0 "\/" v1) "/\" (v0 "\/" v1)

proof

let v1, v0 be Element of L; :: thesis:
(v0 "/\" (v0 "\/" v1)) "\/" (v0 "\/" v1) = (v0 "\/" v1) "\/" (v0 "/\" (v0 "\/" v1)) by A8;
hence (v0 "\/" v1) "\/" (v0 "/\" (v0 "\/" v1)) = (v0 "\/" v1) "/\" (v0 "\/" v1) by A120; :: thesis:

end;

A124: for v1, v0 being Element of L holds v0 "\/" (v1 "\/" (v0 "/\" (v0 "\/" v1))) = (v0 "\/" v1) "/\" (v0 "\/" v1)

proof

let v1, v0 be Element of L; :: thesis:
(v0 "\/" v1) "\/" (v0 "/\" (v0 "\/" v1)) = v0 "\/" (v1 "\/" (v0 "/\" (v0 "\/" v1))) by A7;
hence v0 "\/" (v1 "\/" (v0 "/\" (v0 "\/" v1))) = (v0 "\/" v1) "/\" (v0 "\/" v1) by A122; :: thesis:

end;

A126: for v1, v0 being Element of L holds v0 "\/" (v1 "\/" (v0 "/\" (v0 "\/" v1))) = v0 "\/" v1

proof

let v1, v0 be Element of L; :: thesis:
(v0 "\/" v1) "/\" (v0 "\/" v1) = v0 "\/" v1 by A2;
hence v0 "\/" (v1 "\/" (v0 "/\" (v0 "\/" v1))) = v0 "\/" v1 by A124; :: thesis:

end;

A128: for v0, v2, v1 being Element of L holds (v1 "/\" v0) "\/" (v0 "/\" (v1 "\/" v2)) = v0 "/\" (v1 "\/" v2)

proof

let v0, v2, v1 be Element of L; :: thesis:
v0 "/\" v1 = v1 "/\" v0 by A4;
hence (v1 "/\" v0) "\/" (v0 "/\" (v1 "\/" v2)) = v0 "/\" (v1 "\/" v2) by A23; :: thesis:

end;

A131: for v0, v2, v1 being Element of L holds (v0 "/\" v1) "\/" ((v1 "\/" v2) "/\" v0) = v0 "/\" (v1 "\/" v2)

proof

let v0, v2, v1 be Element of L; :: thesis:
v0 "/\" (v1 "\/" v2) = (v1 "\/" v2) "/\" v0 by A4;
hence (v0 "/\" v1) "\/" ((v1 "\/" v2) "/\" v0) = v0 "/\" (v1 "\/" v2) by A23; :: thesis:

end;

A133: for v0, v1, v2 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" (v2 "\/" v1)) = v0 "/\" (v1 "\/" v2)

proof

let v0, v1, v2 be Element of L; :: thesis:
v1 "\/" v2 = v2 "\/" v1 by A8;
hence (v0 "/\" v1) "\/" (v0 "/\" (v2 "\/" v1)) = v0 "/\" (v1 "\/" v2) by A23; :: thesis:

end;

A136: for v101, v2, v1 being Element of L holds ((v101 "/\" v1) "\/" v101) "/\" (v101 "/\" (v1 "\/" v2)) = (v101 "/\" v1) "\/" (v101 "/\" (v1 "\/" v2))

proof

let v101, v2, v1 be Element of L; :: thesis:
(v101 "/\" v1) "\/" (v101 "/\" (v1 "\/" v2)) = v101 "/\" (v1 "\/" v2) by A23;
hence ((v101 "/\" v1) "\/" v101) "/\" (v101 "/\" (v1 "\/" v2)) = (v101 "/\" v1) "\/" (v101 "/\" (v1 "\/" v2)) by A11; :: thesis:

end;

A139: for v0, v2, v1 being Element of L holds (v0 "\/" (v0 "/\" v1)) "/\" (v0 "/\" (v1 "\/" v2)) = (v0 "/\" v1) "\/" (v0 "/\" (v1 "\/" v2))

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "/\" v1) "\/" v0 = v0 "\/" (v0 "/\" v1) by A8;
hence (v0 "\/" (v0 "/\" v1)) "/\" (v0 "/\" (v1 "\/" v2)) = (v0 "/\" v1) "\/" (v0 "/\" (v1 "\/" v2)) by A136; :: thesis:

end;

A141: for v2, v1, v0 being Element of L holds v0 "/\" ((v0 "\/" (v0 "/\" v1)) "/\" (v1 "\/" v2)) = (v0 "/\" v1) "\/" (v0 "/\" (v1 "\/" v2))

proof

let v2, v1, v0 be Element of L; :: thesis:
(v0 "\/" (v0 "/\" v1)) "/\" (v0 "/\" (v1 "\/" v2)) = v0 "/\" ((v0 "\/" (v0 "/\" v1)) "/\" (v1 "\/" v2)) by A40;
hence v0 "/\" ((v0 "\/" (v0 "/\" v1)) "/\" (v1 "\/" v2)) = (v0 "/\" v1) "\/" (v0 "/\" (v1 "\/" v2)) by A139; :: thesis:

end;

A143: for v2, v1, v0 being Element of L holds v0 "/\" ((v0 "\/" (v0 "/\" v1)) "/\" (v1 "\/" v2)) = v0 "/\" (v1 "\/" v2)

proof

let v2, v1, v0 be Element of L; :: thesis:
(v0 "/\" v1) "\/" (v0 "/\" (v1 "\/" v2)) = v0 "/\" (v1 "\/" v2) by A23;
hence v0 "/\" ((v0 "\/" (v0 "/\" v1)) "/\" (v1 "\/" v2)) = v0 "/\" (v1 "\/" v2) by A141; :: thesis:

end;

A146: for v101, v2, v1 being Element of L holds ((v101 "\/" v1) "/\" v101) "\/" (v101 "\/" (v1 "/\" v2)) = (v101 "\/" v1) "/\" (v101 "\/" (v1 "/\" v2))

proof

let v101, v2, v1 be Element of L; :: thesis:
(v101 "\/" v1) "/\" (v101 "\/" (v1 "/\" v2)) = v101 "\/" (v1 "/\" v2) by A11;
hence ((v101 "\/" v1) "/\" v101) "\/" (v101 "\/" (v1 "/\" v2)) = (v101 "\/" v1) "/\" (v101 "\/" (v1 "/\" v2)) by A23; :: thesis:

end;

A149: for v0, v2, v1 being Element of L holds (v0 "/\" (v0 "\/" v1)) "\/" (v0 "\/" (v1 "/\" v2)) = (v0 "\/" v1) "/\" (v0 "\/" (v1 "/\" v2))

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "\/" v1) "/\" v0 = v0 "/\" (v0 "\/" v1) by A4;
hence (v0 "/\" (v0 "\/" v1)) "\/" (v0 "\/" (v1 "/\" v2)) = (v0 "\/" v1) "/\" (v0 "\/" (v1 "/\" v2)) by A146; :: thesis:

end;

A151: for v2, v1, v0 being Element of L holds v0 "\/" ((v0 "/\" (v0 "\/" v1)) "\/" (v1 "/\" v2)) = (v0 "\/" v1) "/\" (v0 "\/" (v1 "/\" v2))

proof

let v2, v1, v0 be Element of L; :: thesis:
(v0 "/\" (v0 "\/" v1)) "\/" (v0 "\/" (v1 "/\" v2)) = v0 "\/" ((v0 "/\" (v0 "\/" v1)) "\/" (v1 "/\" v2)) by A57;
hence v0 "\/" ((v0 "/\" (v0 "\/" v1)) "\/" (v1 "/\" v2)) = (v0 "\/" v1) "/\" (v0 "\/" (v1 "/\" v2)) by A149; :: thesis:

end;

A153: for v2, v1, v0 being Element of L holds v0 "\/" ((v0 "/\" (v0 "\/" v1)) "\/" (v1 "/\" v2)) = v0 "\/" (v1 "/\" v2)

proof

let v2, v1, v0 be Element of L; :: thesis:
(v0 "\/" v1) "/\" (v0 "\/" (v1 "/\" v2)) = v0 "\/" (v1 "/\" v2) by A11;
hence v0 "\/" ((v0 "/\" (v0 "\/" v1)) "\/" (v1 "/\" v2)) = v0 "\/" (v1 "/\" v2) by A151; :: thesis:

end;

A156: for v1, v101, v100 being Element of L holds (v100 "/\" v101) "/\" (v101 "/\" v1) = v100 "/\" (v101 "/\" v1)

proof

let v1, v101, v100 be Element of L; :: thesis:
v101 "/\" (v101 "/\" v1) = v101 "/\" v1 by A26;
hence (v100 "/\" v101) "/\" (v101 "/\" v1) = v100 "/\" (v101 "/\" v1) by A3; :: thesis:

end;

A159: for v2, v1, v0 being Element of L holds v1 "/\" ((v0 "/\" v1) "/\" v2) = v0 "/\" (v1 "/\" v2)

proof

let v2, v1, v0 be Element of L; :: thesis:
(v0 "/\" v1) "/\" (v1 "/\" v2) = v1 "/\" ((v0 "/\" v1) "/\" v2) by A40;
hence v1 "/\" ((v0 "/\" v1) "/\" v2) = v0 "/\" (v1 "/\" v2) by A156; :: thesis:

end;

A162: for v1, v2, v0 being Element of L holds v0 "/\" (v1 "/\" (v0 "/\" v2)) = v1 "/\" (v0 "/\" v2)

proof

let v1, v2, v0 be Element of L; :: thesis:
(v1 "/\" v0) "/\" v2 = v1 "/\" (v0 "/\" v2) by A3;
hence v0 "/\" (v1 "/\" (v0 "/\" v2)) = v1 "/\" (v0 "/\" v2) by A159; :: thesis:

end;

A165: for v102, v1, v100 being Element of L holds (v100 "/\" v1) "\/" (v102 "/\" (((v100 "/\" v1) "/\" v102) "\/" v100)) = (v102 "\/" (((v100 "/\" v1) "\/" v102) "/\" v100)) "/\" (v100 "\/" (v100 "/\" v1))

proof

let v102, v1, v100 be Element of L; :: thesis:
v100 "/\" (v100 "/\" v1) = v100 "/\" v1 by A26;
hence (v100 "/\" v1) "\/" (v102 "/\" (((v100 "/\" v1) "/\" v102) "\/" v100)) = (v102 "\/" (((v100 "/\" v1) "\/" v102) "/\" v100)) "/\" (v100 "\/" (v100 "/\" v1)) by A20; :: thesis:

end;

A168: for v0, v2, v1 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" ((v0 "/\" (v1 "/\" v2)) "\/" v0)) = (v2 "\/" (((v0 "/\" v1) "\/" v2) "/\" v0)) "/\" (v0 "\/" (v0 "/\" v1))

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "/\" v1) "/\" v2 = v0 "/\" (v1 "/\" v2) by A3;
hence (v0 "/\" v1) "\/" (v2 "/\" ((v0 "/\" (v1 "/\" v2)) "\/" v0)) = (v2 "\/" (((v0 "/\" v1) "\/" v2) "/\" v0)) "/\" (v0 "\/" (v0 "/\" v1)) by A165; :: thesis:

end;

A170: for v0, v2, v1 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" (v0 "\/" (v0 "/\" (v1 "/\" v2)))) = (v2 "\/" (((v0 "/\" v1) "\/" v2) "/\" v0)) "/\" (v0 "\/" (v0 "/\" v1))

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "/\" (v1 "/\" v2)) "\/" v0 = v0 "\/" (v0 "/\" (v1 "/\" v2)) by A8;
hence (v0 "/\" v1) "\/" (v2 "/\" (v0 "\/" (v0 "/\" (v1 "/\" v2)))) = (v2 "\/" (((v0 "/\" v1) "\/" v2) "/\" v0)) "/\" (v0 "\/" (v0 "/\" v1)) by A168; :: thesis:

end;

A172: for v0, v2, v1 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" (v0 "\/" (v0 "/\" (v1 "/\" v2)))) = (v2 "\/" (v0 "/\" ((v0 "/\" v1) "\/" v2))) "/\" (v0 "\/" (v0 "/\" v1))

proof

let v0, v2, v1 be Element of L; :: thesis:
((v0 "/\" v1) "\/" v2) "/\" v0 = v0 "/\" ((v0 "/\" v1) "\/" v2) by A4;
hence (v0 "/\" v1) "\/" (v2 "/\" (v0 "\/" (v0 "/\" (v1 "/\" v2)))) = (v2 "\/" (v0 "/\" ((v0 "/\" v1) "\/" v2))) "/\" (v0 "\/" (v0 "/\" v1)) by A170; :: thesis:

end;

A174: for v0, v2, v1 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" (v0 "\/" (v0 "/\" (v1 "/\" v2)))) = (v0 "\/" (v0 "/\" v1)) "/\" (v2 "\/" (v0 "/\" ((v0 "/\" v1) "\/" v2)))

proof

let v0, v2, v1 be Element of L; :: thesis:
(v2 "\/" (v0 "/\" ((v0 "/\" v1) "\/" v2))) "/\" (v0 "\/" (v0 "/\" v1)) = (v0 "\/" (v0 "/\" v1)) "/\" (v2 "\/" (v0 "/\" ((v0 "/\" v1) "\/" v2))) by A4;
hence (v0 "/\" v1) "\/" (v2 "/\" (v0 "\/" (v0 "/\" (v1 "/\" v2)))) = (v0 "\/" (v0 "/\" v1)) "/\" (v2 "\/" (v0 "/\" ((v0 "/\" v1) "\/" v2))) by A172; :: thesis:

end;

A177: for v0, v100, v1 being Element of L holds v100 "/\" (v0 "/\" (v1 "/\" v100)) = (v0 "/\" v1) "/\" v100

proof

let v0, v100, v1 be Element of L; :: thesis:
(v0 "/\" v1) "/\" v100 = v0 "/\" (v1 "/\" v100) by A3;
hence v100 "/\" (v0 "/\" (v1 "/\" v100)) = (v0 "/\" v1) "/\" v100 by A34; :: thesis:

end;

A180: for v1, v0, v2 being Element of L holds v0 "/\" (v1 "/\" (v2 "/\" v0)) = v1 "/\" (v2 "/\" v0)

proof

let v1, v0, v2 be Element of L; :: thesis:
(v1 "/\" v2) "/\" v0 = v1 "/\" (v2 "/\" v0) by A3;
hence v0 "/\" (v1 "/\" (v2 "/\" v0)) = v1 "/\" (v2 "/\" v0) by A177; :: thesis:

end;

A183: for v100, v101, v1 being Element of L holds (v100 "\/" v101) "/\" (v100 "\/" (v1 "/\" v101)) = v100 "\/" (v101 "/\" (v1 "/\" v101))

proof

let v100, v101, v1 be Element of L; :: thesis:
v101 "/\" (v1 "/\" v101) = v1 "/\" v101 by A34;
hence (v100 "\/" v101) "/\" (v100 "\/" (v1 "/\" v101)) = v100 "\/" (v101 "/\" (v1 "/\" v101)) by A11; :: thesis:

end;

A186: for v0, v1, v2 being Element of L holds (v0 "\/" v1) "/\" (v0 "\/" (v2 "/\" v1)) = v0 "\/" (v2 "/\" v1)

proof

let v0, v1, v2 be Element of L; :: thesis:
v1 "/\" (v2 "/\" v1) = v2 "/\" v1 by A34;
hence (v0 "\/" v1) "/\" (v0 "\/" (v2 "/\" v1)) = v0 "\/" (v2 "/\" v1) by A183; :: thesis:

end;

A189: for v1, v101, v100 being Element of L holds (v100 "\/" v101) "\/" (v101 "\/" v1) = v100 "\/" (v101 "\/" v1)

proof

let v1, v101, v100 be Element of L; :: thesis:
v101 "\/" (v101 "\/" v1) = v101 "\/" v1 by A43;
hence (v100 "\/" v101) "\/" (v101 "\/" v1) = v100 "\/" (v101 "\/" v1) by A7; :: thesis:

end;

A192: for v2, v1, v0 being Element of L holds v1 "\/" ((v0 "\/" v1) "\/" v2) = v0 "\/" (v1 "\/" v2)

proof

let v2, v1, v0 be Element of L; :: thesis:
(v0 "\/" v1) "\/" (v1 "\/" v2) = v1 "\/" ((v0 "\/" v1) "\/" v2) by A57;
hence v1 "\/" ((v0 "\/" v1) "\/" v2) = v0 "\/" (v1 "\/" v2) by A189; :: thesis:

end;

A195: for v1, v2, v0 being Element of L holds v0 "\/" (v1 "\/" (v0 "\/" v2)) = v1 "\/" (v0 "\/" v2)

proof

let v1, v2, v0 be Element of L; :: thesis:
(v1 "\/" v0) "\/" v2 = v1 "\/" (v0 "\/" v2) by A7;
hence v0 "\/" (v1 "\/" (v0 "\/" v2)) = v1 "\/" (v0 "\/" v2) by A192; :: thesis:

end;

A198: for v102, v1, v100 being Element of L holds (v100 "\/" v1) "/\" (v100 "\/" ((v100 "\/" v1) "/\" v102)) = v100 "\/" ((v100 "\/" v1) "/\" v102)

proof

let v102, v1, v100 be Element of L; :: thesis:
v100 "\/" (v100 "\/" v1) = v100 "\/" v1 by A43;
hence (v100 "\/" v1) "/\" (v100 "\/" ((v100 "\/" v1) "/\" v102)) = v100 "\/" ((v100 "\/" v1) "/\" v102) by A11; :: thesis:

end;

A202: for v0, v100, v1 being Element of L holds v100 "\/" (v0 "\/" (v1 "\/" v100)) = (v0 "\/" v1) "\/" v100

proof

let v0, v100, v1 be Element of L; :: thesis:
(v0 "\/" v1) "\/" v100 = v0 "\/" (v1 "\/" v100) by A7;
hence v100 "\/" (v0 "\/" (v1 "\/" v100)) = (v0 "\/" v1) "\/" v100 by A51; :: thesis:

end;

A205: for v1, v0, v2 being Element of L holds v0 "\/" (v1 "\/" (v2 "\/" v0)) = v1 "\/" (v2 "\/" v0)

proof

let v1, v0, v2 be Element of L; :: thesis:
(v1 "\/" v2) "\/" v0 = v1 "\/" (v2 "\/" v0) by A7;
hence v0 "\/" (v1 "\/" (v2 "\/" v0)) = v1 "\/" (v2 "\/" v0) by A202; :: thesis:

end;

A208: for v102, v100, v1 being Element of L holds (v1 "\/" v100) "/\" (v100 "\/" ((v1 "\/" v100) "/\" v102)) = v100 "\/" ((v1 "\/" v100) "/\" v102)

proof

let v102, v100, v1 be Element of L; :: thesis:
v100 "\/" (v1 "\/" v100) = v1 "\/" v100 by A51;
hence (v1 "\/" v100) "/\" (v100 "\/" ((v1 "\/" v100) "/\" v102)) = v100 "\/" ((v1 "\/" v100) "/\" v102) by A11; :: thesis:

end;

A212: for v102, v1, v100 being Element of L holds (v100 "\/" (v100 "/\" v1)) "/\" v102 = v100 "/\" ((v100 "\/" (v100 "/\" v1)) "/\" v102)

proof

let v102, v1, v100 be Element of L; :: thesis:
v100 "/\" (v100 "\/" (v100 "/\" v1)) = v100 "\/" (v100 "/\" v1) by A71;
hence (v100 "\/" (v100 "/\" v1)) "/\" v102 = v100 "/\" ((v100 "\/" (v100 "/\" v1)) "/\" v102) by A3; :: thesis:

end;

A217: for v1, v0 being Element of L holds (v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" ((v0 "/\" v1) "/\" ((v1 "/\" (v0 "/\" v1)) "\/" v0))) = ((v0 "/\" v1) "\/" ((v1 "\/" (v0 "/\" v1)) "/\" v0)) "/\" (v0 "\/" v1)

proof

let v1, v0 be Element of L; :: thesis:
(v0 "/\" v1) "\/" ((v0 "/\" v1) "/\" ((v1 "/\" (v0 "/\" v1)) "\/" v0)) = ((v0 "/\" v1) "\/" ((v1 "\/" (v0 "/\" v1)) "/\" v0)) "/\" (v0 "\/" v1) by A20;
hence (v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" ((v0 "/\" v1) "/\" ((v1 "/\" (v0 "/\" v1)) "\/" v0))) = ((v0 "/\" v1) "\/" ((v1 "\/" (v0 "/\" v1)) "/\" v0)) "/\" (v0 "\/" v1) by A71; :: thesis:

end;

A219: for v1, v0 being Element of L holds (v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" ((v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" v0))) = ((v0 "/\" v1) "\/" ((v1 "\/" (v0 "/\" v1)) "/\" v0)) "/\" (v0 "\/" v1)

proof

let v1, v0 be Element of L; :: thesis:
v1 "/\" (v0 "/\" v1) = v0 "/\" v1 by A34;
hence (v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" ((v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" v0))) = ((v0 "/\" v1) "\/" ((v1 "\/" (v0 "/\" v1)) "/\" v0)) "/\" (v0 "\/" v1) by A217; :: thesis:

end;

A221: for v1, v0 being Element of L holds (v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" ((v0 "/\" v1) "/\" (v0 "\/" (v0 "/\" v1)))) = ((v0 "/\" v1) "\/" ((v1 "\/" (v0 "/\" v1)) "/\" v0)) "/\" (v0 "\/" v1)

proof

let v1, v0 be Element of L; :: thesis:
(v0 "/\" v1) "\/" v0 = v0 "\/" (v0 "/\" v1) by A8;
hence (v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" ((v0 "/\" v1) "/\" (v0 "\/" (v0 "/\" v1)))) = ((v0 "/\" v1) "\/" ((v1 "\/" (v0 "/\" v1)) "/\" v0)) "/\" (v0 "\/" v1) by A219; :: thesis:

end;

A223: for v1, v0 being Element of L holds (v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" (v0 "/\" (v1 "/\" (v0 "\/" (v0 "/\" v1))))) = ((v0 "/\" v1) "\/" ((v1 "\/" (v0 "/\" v1)) "/\" v0)) "/\" (v0 "\/" v1)

proof

let v1, v0 be Element of L; :: thesis:
(v0 "/\" v1) "/\" (v0 "\/" (v0 "/\" v1)) = v0 "/\" (v1 "/\" (v0 "\/" (v0 "/\" v1))) by A3;
hence (v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" (v0 "/\" (v1 "/\" (v0 "\/" (v0 "/\" v1))))) = ((v0 "/\" v1) "\/" ((v1 "\/" (v0 "/\" v1)) "/\" v0)) "/\" (v0 "\/" v1) by A221; :: thesis:

end;

A225: for v1, v0 being Element of L holds (v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" (v0 "/\" v1)) = ((v0 "/\" v1) "\/" ((v1 "\/" (v0 "/\" v1)) "/\" v0)) "/\" (v0 "\/" v1)

proof

let v1, v0 be Element of L; :: thesis:
v0 "/\" (v1 "/\" (v0 "\/" (v0 "/\" v1))) = v0 "/\" v1 by A84;
hence (v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" (v0 "/\" v1)) = ((v0 "/\" v1) "\/" ((v1 "\/" (v0 "/\" v1)) "/\" v0)) "/\" (v0 "\/" v1) by A223; :: thesis:

end;

A227: for v1, v0 being Element of L holds (v0 "/\" v1) "/\" (v0 "/\" v1) = ((v0 "/\" v1) "\/" ((v1 "\/" (v0 "/\" v1)) "/\" v0)) "/\" (v0 "\/" v1)

proof

let v1, v0 be Element of L; :: thesis:
(v0 "/\" v1) "\/" (v0 "/\" v1) = v0 "/\" v1 by A6;
hence (v0 "/\" v1) "/\" (v0 "/\" v1) = ((v0 "/\" v1) "\/" ((v1 "\/" (v0 "/\" v1)) "/\" v0)) "/\" (v0 "\/" v1) by A225; :: thesis:

end;

A229: for v1, v0 being Element of L holds v0 "/\" v1 = ((v0 "/\" v1) "\/" ((v1 "\/" (v0 "/\" v1)) "/\" v0)) "/\" (v0 "\/" v1)

proof

let v1, v0 be Element of L; :: thesis:
(v0 "/\" v1) "/\" (v0 "/\" v1) = v0 "/\" v1 by A2;
hence v0 "/\" v1 = ((v0 "/\" v1) "\/" ((v1 "\/" (v0 "/\" v1)) "/\" v0)) "/\" (v0 "\/" v1) by A227; :: thesis:

end;

A231: for v1, v0 being Element of L holds v0 "/\" v1 = ((v0 "/\" v1) "\/" (v0 "/\" (v1 "\/" (v0 "/\" v1)))) "/\" (v0 "\/" v1)

proof

let v1, v0 be Element of L; :: thesis:
(v1 "\/" (v0 "/\" v1)) "/\" v0 = v0 "/\" (v1 "\/" (v0 "/\" v1)) by A4;
hence v0 "/\" v1 = ((v0 "/\" v1) "\/" (v0 "/\" (v1 "\/" (v0 "/\" v1)))) "/\" (v0 "\/" v1) by A229; :: thesis:

end;

A233: for v1, v0 being Element of L holds v0 "/\" v1 = (v0 "/\" (v1 "\/" (v0 "/\" v1))) "/\" (v0 "\/" v1)

proof

let v1, v0 be Element of L; :: thesis:
(v0 "/\" v1) "\/" (v0 "/\" (v1 "\/" (v0 "/\" v1))) = v0 "/\" (v1 "\/" (v0 "/\" v1)) by A23;
hence v0 "/\" v1 = (v0 "/\" (v1 "\/" (v0 "/\" v1))) "/\" (v0 "\/" v1) by A231; :: thesis:

end;

A235: for v1, v0 being Element of L holds v0 "/\" v1 = v0 "/\" ((v1 "\/" (v0 "/\" v1)) "/\" (v0 "\/" v1))

proof

let v1, v0 be Element of L; :: thesis:
(v0 "/\" (v1 "\/" (v0 "/\" v1))) "/\" (v0 "\/" v1) = v0 "/\" ((v1 "\/" (v0 "/\" v1)) "/\" (v0 "\/" v1)) by A3;
hence v0 "/\" v1 = v0 "/\" ((v1 "\/" (v0 "/\" v1)) "/\" (v0 "\/" v1)) by A233; :: thesis:

end;

A239: for v100, v1, v101 being Element of L holds v100 "/\" (v101 "\/" (v101 "/\" v1)) = v101 "/\" (v100 "/\" (v101 "\/" (v101 "/\" v1)))

proof

let v100, v1, v101 be Element of L; :: thesis:
v101 "/\" (v101 "\/" (v101 "/\" v1)) = v101 "\/" (v101 "/\" v1) by A71;
hence v100 "/\" (v101 "\/" (v101 "/\" v1)) = v101 "/\" (v100 "/\" (v101 "\/" (v101 "/\" v1))) by A40; :: thesis:

end;

A244: for v2, v1, v0 being Element of L holds (v0 "\/" (v0 "/\" v1)) "/\" (v1 "\/" v2) = v0 "/\" (v1 "\/" v2)

proof

let v2, v1, v0 be Element of L; :: thesis:
v0 "/\" ((v0 "\/" (v0 "/\" v1)) "/\" (v1 "\/" v2)) = (v0 "\/" (v0 "/\" v1)) "/\" (v1 "\/" v2) by A212;
hence (v0 "\/" (v0 "/\" v1)) "/\" (v1 "\/" v2) = v0 "/\" (v1 "\/" v2) by A143; :: thesis:

end;

A246: for v1, v0 being Element of L holds v1 "/\" (v0 "\/" (v0 "/\" v1)) = v0 "/\" v1

proof

let v1, v0 be Element of L; :: thesis:
v0 "/\" (v1 "/\" (v0 "\/" (v0 "/\" v1))) = v1 "/\" (v0 "\/" (v0 "/\" v1)) by A239;
hence v1 "/\" (v0 "\/" (v0 "/\" v1)) = v0 "/\" v1 by A84; :: thesis:

end;

A249: for v1, v0 being Element of L holds v0 "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" (v0 "/\" (v0 "\/" v1)))

proof

let v1, v0 be Element of L; :: thesis:
v1 "/\" (v0 "\/" (v0 "/\" v1)) = v0 "/\" v1 by A246;
hence v0 "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" (v0 "/\" (v0 "\/" v1))) by A99; :: thesis:

end;

A251: for v1, v0 being Element of L holds v0 "/\" (v1 "\/" (v0 "/\" v1)) = v1 "/\" v0

proof

let v1, v0 be Element of L; :: thesis:
v1 "/\" v0 = v0 "/\" v1 by A4;
hence v0 "/\" (v1 "\/" (v0 "/\" v1)) = v1 "/\" v0 by A246; :: thesis:

end;

A254: for v1, v0 being Element of L holds ((v1 "/\" (v0 "/\" v1)) "\/" v0) "/\" (((v0 "/\" v1) "\/" ((v1 "\/" (v0 "/\" v1)) "/\" v0)) "/\" (v0 "\/" v1)) = (v0 "/\" v1) "/\" ((v1 "/\" (v0 "/\" v1)) "\/" v0)

proof

let v1, v0 be Element of L; :: thesis:
(v0 "/\" v1) "\/" ((v0 "/\" v1) "/\" ((v1 "/\" (v0 "/\" v1)) "\/" v0)) = ((v0 "/\" v1) "\/" ((v1 "\/" (v0 "/\" v1)) "/\" v0)) "/\" (v0 "\/" v1) by A20;
hence ((v1 "/\" (v0 "/\" v1)) "\/" v0) "/\" (((v0 "/\" v1) "\/" ((v1 "\/" (v0 "/\" v1)) "/\" v0)) "/\" (v0 "\/" v1)) = (v0 "/\" v1) "/\" ((v1 "/\" (v0 "/\" v1)) "\/" v0) by A246; :: thesis:

end;

A257: for v0, v1 being Element of L holds ((v1 "/\" v0) "\/" v1) "/\" (((v1 "/\" v0) "\/" ((v0 "\/" (v1 "/\" v0)) "/\" v1)) "/\" (v1 "\/" v0)) = (v1 "/\" v0) "/\" ((v0 "/\" (v1 "/\" v0)) "\/" v1)

proof

let v0, v1 be Element of L; :: thesis:
v0 "/\" (v1 "/\" v0) = v1 "/\" v0 by A34;
hence ((v1 "/\" v0) "\/" v1) "/\" (((v1 "/\" v0) "\/" ((v0 "\/" (v1 "/\" v0)) "/\" v1)) "/\" (v1 "\/" v0)) = (v1 "/\" v0) "/\" ((v0 "/\" (v1 "/\" v0)) "\/" v1) by A254; :: thesis:

end;

A260: for v1, v0 being Element of L holds (v0 "\/" (v0 "/\" v1)) "/\" (((v0 "/\" v1) "\/" ((v1 "\/" (v0 "/\" v1)) "/\" v0)) "/\" (v0 "\/" v1)) = (v0 "/\" v1) "/\" ((v1 "/\" (v0 "/\" v1)) "\/" v0)

proof

let v1, v0 be Element of L; :: thesis:
(v0 "/\" v1) "\/" v0 = v0 "\/" (v0 "/\" v1) by A8;
hence (v0 "\/" (v0 "/\" v1)) "/\" (((v0 "/\" v1) "\/" ((v1 "\/" (v0 "/\" v1)) "/\" v0)) "/\" (v0 "\/" v1)) = (v0 "/\" v1) "/\" ((v1 "/\" (v0 "/\" v1)) "\/" v0) by A257; :: thesis:

end;

A262: for v1, v0 being Element of L holds (v0 "\/" (v0 "/\" v1)) "/\" (((v0 "/\" v1) "\/" (v0 "/\" (v1 "\/" (v0 "/\" v1)))) "/\" (v0 "\/" v1)) = (v0 "/\" v1) "/\" ((v1 "/\" (v0 "/\" v1)) "\/" v0)

proof

let v1, v0 be Element of L; :: thesis:
(v1 "\/" (v0 "/\" v1)) "/\" v0 = v0 "/\" (v1 "\/" (v0 "/\" v1)) by A4;
hence (v0 "\/" (v0 "/\" v1)) "/\" (((v0 "/\" v1) "\/" (v0 "/\" (v1 "\/" (v0 "/\" v1)))) "/\" (v0 "\/" v1)) = (v0 "/\" v1) "/\" ((v1 "/\" (v0 "/\" v1)) "\/" v0) by A260; :: thesis:

end;

A264: for v1, v0 being Element of L holds (v0 "\/" (v0 "/\" v1)) "/\" (((v0 "/\" v1) "\/" (v1 "/\" v0)) "/\" (v0 "\/" v1)) = (v0 "/\" v1) "/\" ((v1 "/\" (v0 "/\" v1)) "\/" v0)

proof

let v1, v0 be Element of L; :: thesis:
v0 "/\" (v1 "\/" (v0 "/\" v1)) = v1 "/\" v0 by A251;
hence (v0 "\/" (v0 "/\" v1)) "/\" (((v0 "/\" v1) "\/" (v1 "/\" v0)) "/\" (v0 "\/" v1)) = (v0 "/\" v1) "/\" ((v1 "/\" (v0 "/\" v1)) "\/" v0) by A262; :: thesis:

end;

A266: for v1, v0 being Element of L holds (v0 "\/" (v0 "/\" v1)) "/\" ((v0 "\/" v1) "/\" ((v0 "/\" v1) "\/" (v1 "/\" v0))) = (v0 "/\" v1) "/\" ((v1 "/\" (v0 "/\" v1)) "\/" v0)

proof

let v1, v0 be Element of L; :: thesis:
((v0 "/\" v1) "\/" (v1 "/\" v0)) "/\" (v0 "\/" v1) = (v0 "\/" v1) "/\" ((v0 "/\" v1) "\/" (v1 "/\" v0)) by A4;
hence (v0 "\/" (v0 "/\" v1)) "/\" ((v0 "\/" v1) "/\" ((v0 "/\" v1) "\/" (v1 "/\" v0))) = (v0 "/\" v1) "/\" ((v1 "/\" (v0 "/\" v1)) "\/" v0) by A264; :: thesis:

end;

A268: for v1, v0 being Element of L holds (v0 "\/" v1) "/\" ((v0 "\/" (v0 "/\" v1)) "/\" ((v0 "/\" v1) "\/" (v1 "/\" v0))) = (v0 "/\" v1) "/\" ((v1 "/\" (v0 "/\" v1)) "\/" v0)

proof

let v1, v0 be Element of L; :: thesis:
(v0 "\/" (v0 "/\" v1)) "/\" ((v0 "\/" v1) "/\" ((v0 "/\" v1) "\/" (v1 "/\" v0))) = (v0 "\/" v1) "/\" ((v0 "\/" (v0 "/\" v1)) "/\" ((v0 "/\" v1) "\/" (v1 "/\" v0))) by A40;
hence (v0 "\/" v1) "/\" ((v0 "\/" (v0 "/\" v1)) "/\" ((v0 "/\" v1) "\/" (v1 "/\" v0))) = (v0 "/\" v1) "/\" ((v1 "/\" (v0 "/\" v1)) "\/" v0) by A266; :: thesis:

end;

A270: for v1, v0 being Element of L holds (v0 "\/" v1) "/\" ((v0 "\/" (v0 "/\" v1)) "/\" ((v0 "/\" v1) "\/" (v1 "/\" v0))) = (v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" v0)

proof

let v1, v0 be Element of L; :: thesis:
v1 "/\" (v0 "/\" v1) = v0 "/\" v1 by A34;
hence (v0 "\/" v1) "/\" ((v0 "\/" (v0 "/\" v1)) "/\" ((v0 "/\" v1) "\/" (v1 "/\" v0))) = (v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" v0) by A268; :: thesis:

end;

A272: for v1, v0 being Element of L holds (v0 "\/" v1) "/\" ((v0 "\/" (v0 "/\" v1)) "/\" ((v0 "/\" v1) "\/" (v1 "/\" v0))) = (v0 "/\" v1) "/\" (v0 "\/" (v0 "/\" v1))

proof

let v1, v0 be Element of L; :: thesis:
(v0 "/\" v1) "\/" v0 = v0 "\/" (v0 "/\" v1) by A8;
hence (v0 "\/" v1) "/\" ((v0 "\/" (v0 "/\" v1)) "/\" ((v0 "/\" v1) "\/" (v1 "/\" v0))) = (v0 "/\" v1) "/\" (v0 "\/" (v0 "/\" v1)) by A270; :: thesis:

end;

A274: for v1, v0 being Element of L holds (v0 "\/" v1) "/\" ((v0 "\/" (v0 "/\" v1)) "/\" ((v0 "/\" v1) "\/" (v1 "/\" v0))) = v0 "/\" (v1 "/\" (v0 "\/" (v0 "/\" v1)))

proof

let v1, v0 be Element of L; :: thesis:
(v0 "/\" v1) "/\" (v0 "\/" (v0 "/\" v1)) = v0 "/\" (v1 "/\" (v0 "\/" (v0 "/\" v1))) by A3;
hence (v0 "\/" v1) "/\" ((v0 "\/" (v0 "/\" v1)) "/\" ((v0 "/\" v1) "\/" (v1 "/\" v0))) = v0 "/\" (v1 "/\" (v0 "\/" (v0 "/\" v1))) by A272; :: thesis:

end;

A276: for v1, v0 being Element of L holds (v0 "\/" v1) "/\" ((v0 "\/" (v0 "/\" v1)) "/\" ((v0 "/\" v1) "\/" (v1 "/\" v0))) = v0 "/\" (v0 "/\" v1)

proof

let v1, v0 be Element of L; :: thesis:
v1 "/\" (v0 "\/" (v0 "/\" v1)) = v0 "/\" v1 by A246;
hence (v0 "\/" v1) "/\" ((v0 "\/" (v0 "/\" v1)) "/\" ((v0 "/\" v1) "\/" (v1 "/\" v0))) = v0 "/\" (v0 "/\" v1) by A274; :: thesis:

end;

A278: for v1, v0 being Element of L holds (v0 "\/" v1) "/\" ((v0 "\/" (v0 "/\" v1)) "/\" ((v0 "/\" v1) "\/" (v1 "/\" v0))) = v0 "/\" v1

proof

let v1, v0 be Element of L; :: thesis:
v0 "/\" (v0 "/\" v1) = v0 "/\" v1 by A26;
hence (v0 "\/" v1) "/\" ((v0 "\/" (v0 "/\" v1)) "/\" ((v0 "/\" v1) "\/" (v1 "/\" v0))) = v0 "/\" v1 by A276; :: thesis:

end;

A281: for v101, v100 being Element of L holds (v100 "/\" v101) "\/" (v101 "/\" v100) = v100 "/\" (v101 "\/" (v101 "/\" v100))

proof

let v101, v100 be Element of L; :: thesis:
v100 "/\" (v101 "\/" (v101 "/\" v100)) = v101 "/\" v100 by A246;
hence (v100 "/\" v101) "\/" (v101 "/\" v100) = v100 "/\" (v101 "\/" (v101 "/\" v100)) by A23; :: thesis:

end;

A284: for v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v1 "/\" v0) = v1 "/\" v0

proof

let v1, v0 be Element of L; :: thesis:
v0 "/\" (v1 "\/" (v1 "/\" v0)) = v1 "/\" v0 by A246;
hence (v0 "/\" v1) "\/" (v1 "/\" v0) = v1 "/\" v0 by A281; :: thesis:

end;

A286: for v1, v0 being Element of L holds (v0 "\/" v1) "/\" ((v0 "\/" (v0 "/\" v1)) "/\" (v1 "/\" v0)) = v0 "/\" v1

proof

let v1, v0 be Element of L; :: thesis:
(v0 "/\" v1) "\/" (v1 "/\" v0) = v1 "/\" v0 by A284;
hence (v0 "\/" v1) "/\" ((v0 "\/" (v0 "/\" v1)) "/\" (v1 "/\" v0)) = v0 "/\" v1 by A278; :: thesis:

end;

A288: for v1, v0 being Element of L holds (v0 "\/" v1) "/\" ((v1 "/\" v0) "/\" (v0 "\/" (v0 "/\" v1))) = v0 "/\" v1

proof

let v1, v0 be Element of L; :: thesis:
(v0 "\/" (v0 "/\" v1)) "/\" (v1 "/\" v0) = (v1 "/\" v0) "/\" (v0 "\/" (v0 "/\" v1)) by A4;
hence (v0 "\/" v1) "/\" ((v1 "/\" v0) "/\" (v0 "\/" (v0 "/\" v1))) = v0 "/\" v1 by A286; :: thesis:

end;

A290: for v1, v0 being Element of L holds (v0 "\/" v1) "/\" (v1 "/\" (v0 "/\" (v0 "\/" (v0 "/\" v1)))) = v0 "/\" v1

proof

let v1, v0 be Element of L; :: thesis:
(v1 "/\" v0) "/\" (v0 "\/" (v0 "/\" v1)) = v1 "/\" (v0 "/\" (v0 "\/" (v0 "/\" v1))) by A3;
hence (v0 "\/" v1) "/\" (v1 "/\" (v0 "/\" (v0 "\/" (v0 "/\" v1)))) = v0 "/\" v1 by A288; :: thesis:

end;

A292: for v1, v0 being Element of L holds (v0 "\/" v1) "/\" (v1 "/\" (v0 "\/" (v0 "/\" v1))) = v0 "/\" v1

proof

let v1, v0 be Element of L; :: thesis:
v0 "/\" (v0 "\/" (v0 "/\" v1)) = v0 "\/" (v0 "/\" v1) by A71;
hence (v0 "\/" v1) "/\" (v1 "/\" (v0 "\/" (v0 "/\" v1))) = v0 "/\" v1 by A290; :: thesis:

end;

A294: for v1, v0 being Element of L holds (v0 "\/" v1) "/\" (v0 "/\" v1) = v0 "/\" v1

proof

let v1, v0 be Element of L; :: thesis:
v1 "/\" (v0 "\/" (v0 "/\" v1)) = v0 "/\" v1 by A246;
hence (v0 "\/" v1) "/\" (v0 "/\" v1) = v0 "/\" v1 by A292; :: thesis:

end;

A296: for v1, v0 being Element of L holds (v0 "/\" v1) "/\" (v0 "\/" v1) = v0 "/\" v1

proof

let v1, v0 be Element of L; :: thesis:
(v0 "\/" v1) "/\" (v0 "/\" v1) = (v0 "/\" v1) "/\" (v0 "\/" v1) by A4;
hence (v0 "/\" v1) "/\" (v0 "\/" v1) = v0 "/\" v1 by A294; :: thesis:

end;

A298: for v1, v0 being Element of L holds v0 "/\" (v1 "/\" (v0 "\/" v1)) = v0 "/\" v1

proof

let v1, v0 be Element of L; :: thesis:
(v0 "/\" v1) "/\" (v0 "\/" v1) = v0 "/\" (v1 "/\" (v0 "\/" v1)) by A3;
hence v0 "/\" (v1 "/\" (v0 "\/" v1)) = v0 "/\" v1 by A296; :: thesis:

end;

A301: for v102, v100, v1 being Element of L holds (v1 "/\" v100) "/\" v102 = v100 "/\" ((v1 "\/" (v100 "/\" v1)) "/\" v102)

proof

let v102, v100, v1 be Element of L; :: thesis:
v100 "/\" (v1 "\/" (v100 "/\" v1)) = v1 "/\" v100 by A251;
hence (v1 "/\" v100) "/\" v102 = v100 "/\" ((v1 "\/" (v100 "/\" v1)) "/\" v102) by A3; :: thesis:

end;

A304: for v0, v2, v1 being Element of L holds v0 "/\" (v1 "/\" v2) = v1 "/\" ((v0 "\/" (v1 "/\" v0)) "/\" v2)

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "/\" v1) "/\" v2 = v0 "/\" (v1 "/\" v2) by A3;
hence v0 "/\" (v1 "/\" v2) = v1 "/\" ((v0 "\/" (v1 "/\" v0)) "/\" v2) by A301; :: thesis:

end;

A308: for v1, v0 being Element of L holds v1 "/\" (v0 "/\" (v0 "\/" v1)) = v0 "/\" v1

proof

let v1, v0 be Element of L; :: thesis:
v0 "/\" ((v1 "\/" (v0 "/\" v1)) "/\" (v0 "\/" v1)) = v1 "/\" (v0 "/\" (v0 "\/" v1)) by A304;
hence v1 "/\" (v0 "/\" (v0 "\/" v1)) = v0 "/\" v1 by A235; :: thesis:

end;

A312: for v103, v100, v101, v1 being Element of L holds (v100 "\/" v101) "/\" ((v100 "\/" (v1 "/\" v101)) "/\" v103) = (v100 "\/" (v101 "/\" (v1 "/\" v101))) "/\" v103

proof

let v103, v100, v101, v1 be Element of L; :: thesis:
v101 "/\" (v1 "/\" v101) = v1 "/\" v101 by A34;
hence (v100 "\/" v101) "/\" ((v100 "\/" (v1 "/\" v101)) "/\" v103) = (v100 "\/" (v101 "/\" (v1 "/\" v101))) "/\" v103 by A60; :: thesis:

end;

A315: for v3, v0, v1, v2 being Element of L holds (v0 "\/" v1) "/\" ((v0 "\/" (v2 "/\" v1)) "/\" v3) = (v0 "\/" (v2 "/\" v1)) "/\" v3

proof

let v3, v0, v1, v2 be Element of L; :: thesis:
v1 "/\" (v2 "/\" v1) = v2 "/\" v1 by A34;
hence (v0 "\/" v1) "/\" ((v0 "\/" (v2 "/\" v1)) "/\" v3) = (v0 "\/" (v2 "/\" v1)) "/\" v3 by A312; :: thesis:

end;

A318: for v102, v100, v1 being Element of L holds (v1 "/\" v100) "/\" v102 = v100 "/\" ((v1 "/\" (v1 "\/" v100)) "/\" v102)

proof

let v102, v100, v1 be Element of L; :: thesis:
v100 "/\" (v1 "/\" (v1 "\/" v100)) = v1 "/\" v100 by A308;
hence (v1 "/\" v100) "/\" v102 = v100 "/\" ((v1 "/\" (v1 "\/" v100)) "/\" v102) by A3; :: thesis:

end;

A321: for v0, v2, v1 being Element of L holds v0 "/\" (v1 "/\" v2) = v1 "/\" ((v0 "/\" (v0 "\/" v1)) "/\" v2)

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "/\" v1) "/\" v2 = v0 "/\" (v1 "/\" v2) by A3;
hence v0 "/\" (v1 "/\" v2) = v1 "/\" ((v0 "/\" (v0 "\/" v1)) "/\" v2) by A318; :: thesis:

end;

A323: for v0, v2, v1 being Element of L holds v0 "/\" (v1 "/\" v2) = v1 "/\" (v0 "/\" ((v0 "\/" v1) "/\" v2))

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "/\" (v0 "\/" v1)) "/\" v2 = v0 "/\" ((v0 "\/" v1) "/\" v2) by A3;
hence v0 "/\" (v1 "/\" v2) = v1 "/\" (v0 "/\" ((v0 "\/" v1) "/\" v2)) by A321; :: thesis:

end;

A328: for v0, v100, v1 being Element of L holds v100 "/\" ((v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" v100))) = (v0 "\/" v1) "/\" v100

proof

let v0, v100, v1 be Element of L; :: thesis:
(v0 "\/" v1) "\/" v100 = v0 "\/" (v1 "\/" v100) by A7;
hence v100 "/\" ((v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" v100))) = (v0 "\/" v1) "/\" v100 by A308; :: thesis:

end;

A332: for v102, v1, v100 being Element of L holds (v100 "/\" (v100 "\/" v1)) "\/" v102 = v100 "\/" ((v100 "/\" (v100 "\/" v1)) "\/" v102)

proof

let v102, v1, v100 be Element of L; :: thesis:
v100 "\/" (v100 "/\" (v100 "\/" v1)) = v100 "/\" (v100 "\/" v1) by A113;
hence (v100 "/\" (v100 "\/" v1)) "\/" v102 = v100 "\/" ((v100 "/\" (v100 "\/" v1)) "\/" v102) by A7; :: thesis:

end;

A337: for v100, v1, v101 being Element of L holds v100 "\/" (v101 "/\" (v101 "\/" v1)) = v101 "\/" (v100 "\/" (v101 "/\" (v101 "\/" v1)))

proof

let v100, v1, v101 be Element of L; :: thesis:
v101 "\/" (v101 "/\" (v101 "\/" v1)) = v101 "/\" (v101 "\/" v1) by A113;
hence v100 "\/" (v101 "/\" (v101 "\/" v1)) = v101 "\/" (v100 "\/" (v101 "/\" (v101 "\/" v1))) by A57; :: thesis:

end;

A342: for v2, v1, v0 being Element of L holds (v0 "/\" (v0 "\/" v1)) "\/" (v1 "/\" v2) = v0 "\/" (v1 "/\" v2)

proof

let v2, v1, v0 be Element of L; :: thesis:
v0 "\/" ((v0 "/\" (v0 "\/" v1)) "\/" (v1 "/\" v2)) = (v0 "/\" (v0 "\/" v1)) "\/" (v1 "/\" v2) by A332;
hence (v0 "/\" (v0 "\/" v1)) "\/" (v1 "/\" v2) = v0 "\/" (v1 "/\" v2) by A153; :: thesis:

end;

A344: for v1, v0 being Element of L holds v1 "\/" (v0 "/\" (v0 "\/" v1)) = v0 "\/" v1

proof

let v1, v0 be Element of L; :: thesis:
v0 "\/" (v1 "\/" (v0 "/\" (v0 "\/" v1))) = v1 "\/" (v0 "/\" (v0 "\/" v1)) by A337;
hence v1 "\/" (v0 "/\" (v0 "\/" v1)) = v0 "\/" v1 by A126; :: thesis:

end;

A347: for v1, v0 being Element of L holds v0 "\/" (v0 "/\" v1) = v0 "/\" (v0 "\/" v1)

proof

let v1, v0 be Element of L; :: thesis:
v1 "\/" (v0 "/\" (v0 "\/" v1)) = v0 "\/" v1 by A344;
hence v0 "\/" (v0 "/\" v1) = v0 "/\" (v0 "\/" v1) by A249; :: thesis:

end;

A349: for v2, v1, v0 being Element of L holds (v0 "/\" (v0 "\/" v1)) "/\" (v1 "\/" v2) = v0 "/\" (v1 "\/" v2)

proof

let v2, v1, v0 be Element of L; :: thesis:
v0 "\/" (v0 "/\" v1) = v0 "/\" (v0 "\/" v1) by A347;
hence (v0 "/\" (v0 "\/" v1)) "/\" (v1 "\/" v2) = v0 "/\" (v1 "\/" v2) by A244; :: thesis:

end;

A351: for v2, v1, v0 being Element of L holds v0 "/\" ((v0 "\/" v1) "/\" (v1 "\/" v2)) = v0 "/\" (v1 "\/" v2)

proof

let v2, v1, v0 be Element of L; :: thesis:
(v0 "/\" (v0 "\/" v1)) "/\" (v1 "\/" v2) = v0 "/\" ((v0 "\/" v1) "/\" (v1 "\/" v2)) by A3;
hence v0 "/\" ((v0 "\/" v1) "/\" (v1 "\/" v2)) = v0 "/\" (v1 "\/" v2) by A349; :: thesis:

end;

A353: for v0, v2, v1 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" (v0 "/\" (v0 "\/" (v1 "/\" v2)))) = (v0 "\/" (v0 "/\" v1)) "/\" (v2 "\/" (v0 "/\" ((v0 "/\" v1) "\/" v2)))

proof

let v0, v2, v1 be Element of L; :: thesis:
v0 "\/" (v0 "/\" (v1 "/\" v2)) = v0 "/\" (v0 "\/" (v1 "/\" v2)) by A347;
hence (v0 "/\" v1) "\/" (v2 "/\" (v0 "/\" (v0 "\/" (v1 "/\" v2)))) = (v0 "\/" (v0 "/\" v1)) "/\" (v2 "\/" (v0 "/\" ((v0 "/\" v1) "\/" v2))) by A174; :: thesis:

end;

A355: for v0, v2, v1 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" (v0 "/\" (v0 "\/" (v1 "/\" v2)))) = (v0 "/\" (v0 "\/" v1)) "/\" (v2 "\/" (v0 "/\" ((v0 "/\" v1) "\/" v2)))

proof

let v0, v2, v1 be Element of L; :: thesis:
v0 "\/" (v0 "/\" v1) = v0 "/\" (v0 "\/" v1) by A347;
hence (v0 "/\" v1) "\/" (v2 "/\" (v0 "/\" (v0 "\/" (v1 "/\" v2)))) = (v0 "/\" (v0 "\/" v1)) "/\" (v2 "\/" (v0 "/\" ((v0 "/\" v1) "\/" v2))) by A353; :: thesis:

end;

A357: for v0, v2, v1 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" (v0 "/\" (v0 "\/" (v1 "/\" v2)))) = v0 "/\" ((v0 "\/" v1) "/\" (v2 "\/" (v0 "/\" ((v0 "/\" v1) "\/" v2))))

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "/\" (v0 "\/" v1)) "/\" (v2 "\/" (v0 "/\" ((v0 "/\" v1) "\/" v2))) = v0 "/\" ((v0 "\/" v1) "/\" (v2 "\/" (v0 "/\" ((v0 "/\" v1) "\/" v2)))) by A3;
hence (v0 "/\" v1) "\/" (v2 "/\" (v0 "/\" (v0 "\/" (v1 "/\" v2)))) = v0 "/\" ((v0 "\/" v1) "/\" (v2 "\/" (v0 "/\" ((v0 "/\" v1) "\/" v2)))) by A355; :: thesis:

end;

A360: for v101, v100 being Element of L holds (v100 "\/" v101) "/\" (v101 "\/" v100) = v100 "\/" (v101 "/\" (v101 "\/" v100))

proof

let v101, v100 be Element of L; :: thesis:
v100 "\/" (v101 "/\" (v101 "\/" v100)) = v101 "\/" v100 by A344;
hence (v100 "\/" v101) "/\" (v101 "\/" v100) = v100 "\/" (v101 "/\" (v101 "\/" v100)) by A11; :: thesis:

end;

A363: for v1, v0 being Element of L holds (v0 "\/" v1) "/\" (v1 "\/" v0) = v1 "\/" v0

proof

let v1, v0 be Element of L; :: thesis:
v0 "\/" (v1 "/\" (v1 "\/" v0)) = v1 "\/" v0 by A344;
hence (v0 "\/" v1) "/\" (v1 "\/" v0) = v1 "\/" v0 by A360; :: thesis:

end;

A366: for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" ((v0 "/\" v1) "/\" (v0 "/\" (v1 "\/" v2))) = (v0 "/\" v1) "\/" (v0 "/\" (v1 "\/" v2))

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "/\" v1) "\/" (v0 "/\" (v1 "\/" v2)) = v0 "/\" (v1 "\/" v2) by A23;
hence (v0 "/\" (v1 "\/" v2)) "\/" ((v0 "/\" v1) "/\" (v0 "/\" (v1 "\/" v2))) = (v0 "/\" v1) "\/" (v0 "/\" (v1 "\/" v2)) by A344; :: thesis:

end;

A368: for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" ((v0 "/\" v1) "/\" (v1 "\/" v2))) = (v0 "/\" v1) "\/" (v0 "/\" (v1 "\/" v2))

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "/\" v1) "/\" (v0 "/\" (v1 "\/" v2)) = v0 "/\" ((v0 "/\" v1) "/\" (v1 "\/" v2)) by A40;
hence (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" ((v0 "/\" v1) "/\" (v1 "\/" v2))) = (v0 "/\" v1) "\/" (v0 "/\" (v1 "\/" v2)) by A366; :: thesis:

end;

A370: for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" (v0 "/\" (v1 "/\" (v1 "\/" v2)))) = (v0 "/\" v1) "\/" (v0 "/\" (v1 "\/" v2))

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "/\" v1) "/\" (v1 "\/" v2) = v0 "/\" (v1 "/\" (v1 "\/" v2)) by A3;
hence (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" (v0 "/\" (v1 "/\" (v1 "\/" v2)))) = (v0 "/\" v1) "\/" (v0 "/\" (v1 "\/" v2)) by A368; :: thesis:

end;

A372: for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" (v1 "/\" (v1 "\/" v2))) = (v0 "/\" v1) "\/" (v0 "/\" (v1 "\/" v2))

proof

let v0, v2, v1 be Element of L; :: thesis:
v0 "/\" (v0 "/\" (v1 "/\" (v1 "\/" v2))) = v0 "/\" (v1 "/\" (v1 "\/" v2)) by A26;
hence (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" (v1 "/\" (v1 "\/" v2))) = (v0 "/\" v1) "\/" (v0 "/\" (v1 "\/" v2)) by A370; :: thesis:

end;

A374: for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" (v1 "/\" (v1 "\/" v2))) = v0 "/\" (v1 "\/" v2)

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "/\" v1) "\/" (v0 "/\" (v1 "\/" v2)) = v0 "/\" (v1 "\/" v2) by A23;
hence (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" (v1 "/\" (v1 "\/" v2))) = v0 "/\" (v1 "\/" v2) by A372; :: thesis:

end;

A377: for v101, v1 being Element of L holds (v1 "\/" v101) "\/" (v101 "/\" (v1 "\/" v101)) = v101 "\/" (v1 "\/" v101)

proof

let v101, v1 be Element of L; :: thesis:
v101 "\/" (v1 "\/" v101) = v1 "\/" v101 by A51;
hence (v1 "\/" v101) "\/" (v101 "/\" (v1 "\/" v101)) = v101 "\/" (v1 "\/" v101) by A344; :: thesis:

end;

A380: for v1, v0 being Element of L holds v0 "\/" (v1 "\/" (v1 "/\" (v0 "\/" v1))) = v1 "\/" (v0 "\/" v1)

proof

let v1, v0 be Element of L; :: thesis:
(v0 "\/" v1) "\/" (v1 "/\" (v0 "\/" v1)) = v0 "\/" (v1 "\/" (v1 "/\" (v0 "\/" v1))) by A7;
hence v0 "\/" (v1 "\/" (v1 "/\" (v0 "\/" v1))) = v1 "\/" (v0 "\/" v1) by A377; :: thesis:

end;

A382: for v1, v0 being Element of L holds v0 "\/" (v1 "/\" (v1 "\/" (v0 "\/" v1))) = v1 "\/" (v0 "\/" v1)

proof

let v1, v0 be Element of L; :: thesis:
v1 "\/" (v1 "/\" (v0 "\/" v1)) = v1 "/\" (v1 "\/" (v0 "\/" v1)) by A347;
hence v0 "\/" (v1 "/\" (v1 "\/" (v0 "\/" v1))) = v1 "\/" (v0 "\/" v1) by A380; :: thesis:

end;

A384: for v1, v0 being Element of L holds v0 "\/" (v1 "/\" (v0 "\/" v1)) = v1 "\/" (v0 "\/" v1)

proof

let v1, v0 be Element of L; :: thesis:
v1 "\/" (v0 "\/" v1) = v0 "\/" v1 by A51;
hence v0 "\/" (v1 "/\" (v0 "\/" v1)) = v1 "\/" (v0 "\/" v1) by A382; :: thesis:

end;

A386: for v1, v0 being Element of L holds v0 "\/" (v1 "/\" (v0 "\/" v1)) = v0 "\/" v1

proof

let v1, v0 be Element of L; :: thesis:
v1 "\/" (v0 "\/" v1) = v0 "\/" v1 by A51;
hence v0 "\/" (v1 "/\" (v0 "\/" v1)) = v0 "\/" v1 by A384; :: thesis:

end;

A389: for v103, v100, v101 being Element of L holds (v100 "\/" v101) "/\" ((v101 "\/" v100) "/\" v103) = (v100 "\/" (v101 "/\" (v101 "\/" v100))) "/\" v103

proof

let v103, v100, v101 be Element of L; :: thesis:
v100 "\/" (v101 "/\" (v101 "\/" v100)) = v101 "\/" v100 by A344;
hence (v100 "\/" v101) "/\" ((v101 "\/" v100) "/\" v103) = (v100 "\/" (v101 "/\" (v101 "\/" v100))) "/\" v103 by A60; :: thesis:

end;

A392: for v2, v0, v1 being Element of L holds (v0 "\/" v1) "/\" ((v1 "\/" v0) "/\" v2) = (v1 "\/" v0) "/\" v2

proof

let v2, v0, v1 be Element of L; :: thesis:
v0 "\/" (v1 "/\" (v1 "\/" v0)) = v1 "\/" v0 by A344;
hence (v0 "\/" v1) "/\" ((v1 "\/" v0) "/\" v2) = (v1 "\/" v0) "/\" v2 by A389; :: thesis:

end;

A395: for v0, v101, v1 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" (v1 "/\" v101)) = (v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" v101)

proof

let v0, v101, v1 be Element of L; :: thesis:
(v0 "/\" v1) "/\" v101 = v0 "/\" (v1 "/\" v101) by A3;
hence (v0 "/\" v1) "\/" (v0 "/\" (v1 "/\" v101)) = (v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" v101) by A347; :: thesis:

end;

A398: for v0, v2, v1 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" (v1 "/\" v2)) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2))

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" v2) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2)) by A3;
hence (v0 "/\" v1) "\/" (v0 "/\" (v1 "/\" v2)) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2)) by A395; :: thesis:

end;

A400: for v0, v1 being Element of L holds v0 "\/" (v1 "/\" v0) = v0 "/\" (v0 "\/" v1)

proof

let v0, v1 be Element of L; :: thesis:
v0 "/\" v1 = v1 "/\" v0 by A4;
hence v0 "\/" (v1 "/\" v0) = v0 "/\" (v0 "\/" v1) by A347; :: thesis:

end;

A403: for v102, v1, v100 being Element of L holds (v100 "/\" (v100 "\/" v1)) "\/" v102 = v100 "\/" ((v100 "/\" v1) "\/" v102)

proof

let v102, v1, v100 be Element of L; :: thesis:
v100 "\/" (v100 "/\" v1) = v100 "/\" (v100 "\/" v1) by A347;
hence (v100 "/\" (v100 "\/" v1)) "\/" v102 = v100 "\/" ((v100 "/\" v1) "\/" v102) by A7; :: thesis:

end;

A407: for v100, v1, v101 being Element of L holds (v100 "/\" v101) "\/" (v100 "/\" (v101 "/\" (v101 "\/" v1))) = v100 "/\" (v101 "\/" (v101 "/\" v1))

proof

let v100, v1, v101 be Element of L; :: thesis:
v101 "\/" (v101 "/\" v1) = v101 "/\" (v101 "\/" v1) by A347;
hence (v100 "/\" v101) "\/" (v100 "/\" (v101 "/\" (v101 "\/" v1))) = v100 "/\" (v101 "\/" (v101 "/\" v1)) by A23; :: thesis:

end;

A410: for v2, v1, v0 being Element of L holds v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" (v1 "\/" v2))) = v0 "/\" (v1 "\/" (v1 "/\" v2))

proof

let v2, v1, v0 be Element of L; :: thesis:
(v0 "/\" v1) "\/" (v0 "/\" (v1 "/\" (v1 "\/" v2))) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" (v1 "\/" v2))) by A398;
hence v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" (v1 "\/" v2))) = v0 "/\" (v1 "\/" (v1 "/\" v2)) by A407; :: thesis:

end;

A412: for v2, v1, v0 being Element of L holds v0 "/\" (v1 "/\" (v1 "\/" ((v0 "/\" v1) "\/" v2))) = v0 "/\" (v1 "\/" (v1 "/\" v2))

proof

let v2, v1, v0 be Element of L; :: thesis:
(v0 "/\" v1) "\/" (v1 "\/" v2) = v1 "\/" ((v0 "/\" v1) "\/" v2) by A57;
hence v0 "/\" (v1 "/\" (v1 "\/" ((v0 "/\" v1) "\/" v2))) = v0 "/\" (v1 "\/" (v1 "/\" v2)) by A410; :: thesis:

end;

A414: for v2, v1, v0 being Element of L holds v0 "/\" (v1 "/\" (v1 "\/" ((v0 "/\" v1) "\/" v2))) = v0 "/\" (v1 "/\" (v1 "\/" v2))

proof

let v2, v1, v0 be Element of L; :: thesis:
v1 "\/" (v1 "/\" v2) = v1 "/\" (v1 "\/" v2) by A347;
hence v0 "/\" (v1 "/\" (v1 "\/" ((v0 "/\" v1) "\/" v2))) = v0 "/\" (v1 "/\" (v1 "\/" v2)) by A412; :: thesis:

end;

A417: for v1, v2, v100 being Element of L holds v100 "\/" (v1 "/\" (v100 "/\" v2)) = v100 "/\" (v100 "\/" (v1 "/\" v2))

proof

let v1, v2, v100 be Element of L; :: thesis:
v100 "/\" (v1 "/\" v2) = v1 "/\" (v100 "/\" v2) by A40;
hence v100 "\/" (v1 "/\" (v100 "/\" v2)) = v100 "/\" (v100 "\/" (v1 "/\" v2)) by A347; :: thesis:

end;

A421: for v100, v1, v101 being Element of L holds v100 "\/" (v101 "/\" (v101 "\/" v1)) = v101 "\/" (v100 "\/" (v101 "/\" v1))

proof

let v100, v1, v101 be Element of L; :: thesis:
v101 "\/" (v101 "/\" v1) = v101 "/\" (v101 "\/" v1) by A347;
hence v100 "\/" (v101 "/\" (v101 "\/" v1)) = v101 "\/" (v100 "\/" (v101 "/\" v1)) by A57; :: thesis:

end;

A426: for v2, v1, v0 being Element of L holds v0 "\/" ((v0 "/\" v1) "\/" (v1 "/\" v2)) = v0 "\/" (v1 "/\" v2)

proof

let v2, v1, v0 be Element of L; :: thesis:
(v0 "/\" (v0 "\/" v1)) "\/" (v1 "/\" v2) = v0 "\/" ((v0 "/\" v1) "\/" (v1 "/\" v2)) by A403;
hence v0 "\/" ((v0 "/\" v1) "\/" (v1 "/\" v2)) = v0 "\/" (v1 "/\" v2) by A342; :: thesis:

end;

A429: for v100, v102, v101 being Element of L holds (v100 "\/" v101) "/\" ((v101 "/\" v102) "\/" v100) = (v100 "\/" (v101 "/\" v102)) "/\" ((v101 "/\" v102) "\/" v100)

proof

let v100, v102, v101 be Element of L; :: thesis:
(v100 "\/" (v101 "/\" v102)) "/\" ((v101 "/\" v102) "\/" v100) = (v101 "/\" v102) "\/" v100 by A363;
hence (v100 "\/" v101) "/\" ((v101 "/\" v102) "\/" v100) = (v100 "\/" (v101 "/\" v102)) "/\" ((v101 "/\" v102) "\/" v100) by A60; :: thesis:

end;

A432: for v0, v2, v1 being Element of L holds (v0 "\/" v1) "/\" ((v1 "/\" v2) "\/" v0) = (v1 "/\" v2) "\/" v0

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "\/" (v1 "/\" v2)) "/\" ((v1 "/\" v2) "\/" v0) = (v1 "/\" v2) "\/" v0 by A363;
hence (v0 "\/" v1) "/\" ((v1 "/\" v2) "\/" v0) = (v1 "/\" v2) "\/" v0 by A429; :: thesis:

end;

A435: for v100, v101, v1, v0 being Element of L holds (v100 "\/" (v101 "/\" (v0 "\/" v1))) "/\" (v100 "\/" (v101 "/\" (v1 "\/" v0))) = v100 "\/" (v101 "/\" ((v0 "\/" v1) "/\" (v1 "\/" v0)))

proof

let v100, v101, v1, v0 be Element of L; :: thesis:
(v0 "\/" v1) "/\" (v1 "\/" v0) = v1 "\/" v0 by A363;
hence (v100 "\/" (v101 "/\" (v0 "\/" v1))) "/\" (v100 "\/" (v101 "/\" (v1 "\/" v0))) = v100 "\/" (v101 "/\" ((v0 "\/" v1) "/\" (v1 "\/" v0))) by A68; :: thesis:

end;

A438: for v0, v1, v3, v2 being Element of L holds (v0 "\/" (v1 "/\" (v2 "\/" v3))) "/\" (v0 "\/" (v1 "/\" (v3 "\/" v2))) = v0 "\/" (v1 "/\" (v3 "\/" v2))

proof

let v0, v1, v3, v2 be Element of L; :: thesis:
(v2 "\/" v3) "/\" (v3 "\/" v2) = v3 "\/" v2 by A363;
hence (v0 "\/" (v1 "/\" (v2 "\/" v3))) "/\" (v0 "\/" (v1 "/\" (v3 "\/" v2))) = v0 "\/" (v1 "/\" (v3 "\/" v2)) by A435; :: thesis:

end;

A441: for v0, v100, v1 being Element of L holds v100 "\/" (v0 "/\" (v1 "/\" v100)) = v100 "/\" (v100 "\/" (v0 "/\" v1))

proof

let v0, v100, v1 be Element of L; :: thesis:
(v0 "/\" v1) "/\" v100 = v0 "/\" (v1 "/\" v100) by A3;
hence v100 "\/" (v0 "/\" (v1 "/\" v100)) = v100 "/\" (v100 "\/" (v0 "/\" v1)) by A400; :: thesis:

end;

A445: for v1, v2, v101 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" (v101 "/\" v2)) = (v1 "/\" v2) "/\" ((v1 "/\" v2) "\/" v101)

proof

let v1, v2, v101 be Element of L; :: thesis:
v101 "/\" (v1 "/\" v2) = v1 "/\" (v101 "/\" v2) by A40;
hence (v1 "/\" v2) "\/" (v1 "/\" (v101 "/\" v2)) = (v1 "/\" v2) "/\" ((v1 "/\" v2) "\/" v101) by A400; :: thesis:

end;

A448: for v0, v1, v2 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" (v2 "/\" v1)) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2))

proof

let v0, v1, v2 be Element of L; :: thesis:
(v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" v2) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2)) by A3;
hence (v0 "/\" v1) "\/" (v0 "/\" (v2 "/\" v1)) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2)) by A445; :: thesis:

end;

A451: for v100, v1, v101 being Element of L holds v100 "\/" (v101 "/\" (v101 "\/" v1)) = v101 "\/" (v100 "\/" (v1 "/\" v101))

proof

let v100, v1, v101 be Element of L; :: thesis:
v101 "\/" (v1 "/\" v101) = v101 "/\" (v101 "\/" v1) by A400;
hence v100 "\/" (v101 "/\" (v101 "\/" v1)) = v101 "\/" (v100 "\/" (v1 "/\" v101)) by A57; :: thesis:

end;

A456: for v0, v2, v1 being Element of L holds v0 "/\" ((v1 "\/" v2) "/\" ((v0 "/\" (v1 "\/" v2)) "\/" v1)) = v0 "/\" (v1 "\/" v2)

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" (v1 "/\" (v1 "\/" v2))) = v0 "/\" ((v1 "\/" v2) "/\" ((v0 "/\" (v1 "\/" v2)) "\/" v1)) by A448;
hence v0 "/\" ((v1 "\/" v2) "/\" ((v0 "/\" (v1 "\/" v2)) "\/" v1)) = v0 "/\" (v1 "\/" v2) by A374; :: thesis:

end;

A458: for v0, v2, v1 being Element of L holds v0 "/\" ((v1 "\/" v2) "/\" (v1 "\/" (v0 "/\" (v1 "\/" v2)))) = v0 "/\" (v1 "\/" v2)

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "/\" (v1 "\/" v2)) "\/" v1 = v1 "\/" (v0 "/\" (v1 "\/" v2)) by A8;
hence v0 "/\" ((v1 "\/" v2) "/\" (v1 "\/" (v0 "/\" (v1 "\/" v2)))) = v0 "/\" (v1 "\/" v2) by A456; :: thesis:

end;

A461: for v0, v1, v102, v100 being Element of L holds v100 "/\" (v0 "/\" (v1 "/\" (v100 "/\" v102))) = (v0 "/\" v1) "/\" (v100 "/\" v102)

proof

let v0, v1, v102, v100 be Element of L; :: thesis:
(v0 "/\" v1) "/\" (v100 "/\" v102) = v0 "/\" (v1 "/\" (v100 "/\" v102)) by A3;
hence v100 "/\" (v0 "/\" (v1 "/\" (v100 "/\" v102))) = (v0 "/\" v1) "/\" (v100 "/\" v102) by A162; :: thesis:

end;

A464: for v1, v2, v3, v0 being Element of L holds v0 "/\" (v1 "/\" (v2 "/\" (v0 "/\" v3))) = v1 "/\" (v2 "/\" (v0 "/\" v3))

proof

let v1, v2, v3, v0 be Element of L; :: thesis:
(v1 "/\" v2) "/\" (v0 "/\" v3) = v1 "/\" (v2 "/\" (v0 "/\" v3)) by A3;
hence v0 "/\" (v1 "/\" (v2 "/\" (v0 "/\" v3))) = v1 "/\" (v2 "/\" (v0 "/\" v3)) by A461; :: thesis:

end;

A467: for v101, v0, v100, v1 being Element of L holds v100 "/\" (v101 "/\" (v0 "/\" (v1 "/\" v100))) = v101 "/\" ((v0 "/\" v1) "/\" v100)

proof

let v101, v0, v100, v1 be Element of L; :: thesis:
(v0 "/\" v1) "/\" v100 = v0 "/\" (v1 "/\" v100) by A3;
hence v100 "/\" (v101 "/\" (v0 "/\" (v1 "/\" v100))) = v101 "/\" ((v0 "/\" v1) "/\" v100) by A180; :: thesis:

end;

A470: for v1, v2, v0, v3 being Element of L holds v0 "/\" (v1 "/\" (v2 "/\" (v3 "/\" v0))) = v1 "/\" (v2 "/\" (v3 "/\" v0))

proof

let v1, v2, v0, v3 be Element of L; :: thesis:
(v2 "/\" v3) "/\" v0 = v2 "/\" (v3 "/\" v0) by A3;
hence v0 "/\" (v1 "/\" (v2 "/\" (v3 "/\" v0))) = v1 "/\" (v2 "/\" (v3 "/\" v0)) by A467; :: thesis:

end;

A473: for v101, v1, v102 being Element of L holds (v1 "/\" (v102 "\/" v1)) "/\" (v101 "/\" (v102 "/\" v1)) = v101 "/\" (v102 "/\" (v1 "/\" (v102 "\/" v1)))

proof

let v101, v1, v102 be Element of L; :: thesis:
v102 "/\" (v1 "/\" (v102 "\/" v1)) = v102 "/\" v1 by A298;
hence (v1 "/\" (v102 "\/" v1)) "/\" (v101 "/\" (v102 "/\" v1)) = v101 "/\" (v102 "/\" (v1 "/\" (v102 "\/" v1))) by A180; :: thesis:

end;

A476: for v2, v0, v1 being Element of L holds v0 "/\" ((v1 "\/" v0) "/\" (v2 "/\" (v1 "/\" v0))) = v2 "/\" (v1 "/\" (v0 "/\" (v1 "\/" v0)))

proof

let v2, v0, v1 be Element of L; :: thesis:
(v0 "/\" (v1 "\/" v0)) "/\" (v2 "/\" (v1 "/\" v0)) = v0 "/\" ((v1 "\/" v0) "/\" (v2 "/\" (v1 "/\" v0))) by A3;
hence v0 "/\" ((v1 "\/" v0) "/\" (v2 "/\" (v1 "/\" v0))) = v2 "/\" (v1 "/\" (v0 "/\" (v1 "\/" v0))) by A473; :: thesis:

end;

A478: for v2, v0, v1 being Element of L holds (v1 "\/" v0) "/\" (v2 "/\" (v1 "/\" v0)) = v2 "/\" (v1 "/\" (v0 "/\" (v1 "\/" v0)))

proof

let v2, v0, v1 be Element of L; :: thesis:
v0 "/\" ((v1 "\/" v0) "/\" (v2 "/\" (v1 "/\" v0))) = (v1 "\/" v0) "/\" (v2 "/\" (v1 "/\" v0)) by A470;
hence (v1 "\/" v0) "/\" (v2 "/\" (v1 "/\" v0)) = v2 "/\" (v1 "/\" (v0 "/\" (v1 "\/" v0))) by A476; :: thesis:

end;

A481: for v2, v1, v0 being Element of L holds (v0 "\/" v1) "/\" (v2 "/\" (v0 "/\" v1)) = v2 "/\" (v0 "/\" v1)

proof

let v2, v1, v0 be Element of L; :: thesis:
v0 "/\" (v1 "/\" (v0 "\/" v1)) = v0 "/\" v1 by A298;
hence (v0 "\/" v1) "/\" (v2 "/\" (v0 "/\" v1)) = v2 "/\" (v0 "/\" v1) by A478; :: thesis:

end;

A484: for v0, v1, v102, v100 being Element of L holds v100 "\/" (v0 "\/" (v1 "\/" (v100 "\/" v102))) = (v0 "\/" v1) "\/" (v100 "\/" v102)

proof

let v0, v1, v102, v100 be Element of L; :: thesis:
(v0 "\/" v1) "\/" (v100 "\/" v102) = v0 "\/" (v1 "\/" (v100 "\/" v102)) by A7;
hence v100 "\/" (v0 "\/" (v1 "\/" (v100 "\/" v102))) = (v0 "\/" v1) "\/" (v100 "\/" v102) by A195; :: thesis:

end;

A487: for v1, v2, v3, v0 being Element of L holds v0 "\/" (v1 "\/" (v2 "\/" (v0 "\/" v3))) = v1 "\/" (v2 "\/" (v0 "\/" v3))

proof

let v1, v2, v3, v0 be Element of L; :: thesis:
(v1 "\/" v2) "\/" (v0 "\/" v3) = v1 "\/" (v2 "\/" (v0 "\/" v3)) by A7;
hence v0 "\/" (v1 "\/" (v2 "\/" (v0 "\/" v3))) = v1 "\/" (v2 "\/" (v0 "\/" v3)) by A484; :: thesis:

end;

A490: for v101, v102, v1 being Element of L holds (v1 "/\" (v1 "\/" v102)) "\/" (v101 "\/" (v1 "\/" v102)) = v101 "\/" (v102 "\/" (v1 "/\" (v1 "\/" v102)))

proof

let v101, v102, v1 be Element of L; :: thesis:
v102 "\/" (v1 "/\" (v1 "\/" v102)) = v1 "\/" v102 by A344;
hence (v1 "/\" (v1 "\/" v102)) "\/" (v101 "\/" (v1 "\/" v102)) = v101 "\/" (v102 "\/" (v1 "/\" (v1 "\/" v102))) by A205; :: thesis:

end;

A493: for v2, v1, v0 being Element of L holds v0 "\/" ((v0 "/\" v1) "\/" (v2 "\/" (v0 "\/" v1))) = v2 "\/" (v1 "\/" (v0 "/\" (v0 "\/" v1)))

proof

let v2, v1, v0 be Element of L; :: thesis:
(v0 "/\" (v0 "\/" v1)) "\/" (v2 "\/" (v0 "\/" v1)) = v0 "\/" ((v0 "/\" v1) "\/" (v2 "\/" (v0 "\/" v1))) by A403;
hence v0 "\/" ((v0 "/\" v1) "\/" (v2 "\/" (v0 "\/" v1))) = v2 "\/" (v1 "\/" (v0 "/\" (v0 "\/" v1))) by A490; :: thesis:

end;

A495: for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v2 "\/" (v0 "\/" v1)) = v2 "\/" (v1 "\/" (v0 "/\" (v0 "\/" v1)))

proof

let v2, v1, v0 be Element of L; :: thesis:
v0 "\/" ((v0 "/\" v1) "\/" (v2 "\/" (v0 "\/" v1))) = (v0 "/\" v1) "\/" (v2 "\/" (v0 "\/" v1)) by A487;
hence (v0 "/\" v1) "\/" (v2 "\/" (v0 "\/" v1)) = v2 "\/" (v1 "\/" (v0 "/\" (v0 "\/" v1))) by A493; :: thesis:

end;

A497: for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v2 "\/" (v0 "\/" v1)) = v2 "\/" (v0 "\/" v1)

proof

let v2, v1, v0 be Element of L; :: thesis:
v1 "\/" (v0 "/\" (v0 "\/" v1)) = v0 "\/" v1 by A344;
hence (v0 "/\" v1) "\/" (v2 "\/" (v0 "\/" v1)) = v2 "\/" (v0 "\/" v1) by A495; :: thesis:

end;

A500: for v1, v2, v0 being Element of L holds v1 "\/" (v0 "/\" v2) = (v1 "\/" (v0 "/\" v2)) "/\" (v0 "\/" v1)

proof

let v1, v2, v0 be Element of L; :: thesis:
(v0 "\/" v1) "/\" (v1 "\/" (v0 "/\" v2)) = v1 "\/" (v0 "/\" v2) by A86;
hence v1 "\/" (v0 "/\" v2) = (v1 "\/" (v0 "/\" v2)) "/\" (v0 "\/" v1) by A4; :: thesis:

end;

A505: for v102, v1, v100 being Element of L holds (v100 "\/" v1) "/\" ((v100 "\/" v1) "\/" (v100 "/\" v102)) = (v100 "\/" v1) "\/" (v100 "/\" v102)

proof

let v102, v1, v100 be Element of L; :: thesis:
v100 "\/" (v100 "\/" v1) = v100 "\/" v1 by A43;
hence (v100 "\/" v1) "/\" ((v100 "\/" v1) "\/" (v100 "/\" v102)) = (v100 "\/" v1) "\/" (v100 "/\" v102) by A86; :: thesis:

end;

A508: for v1, v2, v0 being Element of L holds (v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" (v0 "/\" v2))) = (v0 "\/" v1) "\/" (v0 "/\" v2)

proof

let v1, v2, v0 be Element of L; :: thesis:
(v0 "\/" v1) "\/" (v0 "/\" v2) = v0 "\/" (v1 "\/" (v0 "/\" v2)) by A7;
hence (v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" (v0 "/\" v2))) = (v0 "\/" v1) "\/" (v0 "/\" v2) by A505; :: thesis:

end;

A510: for v1, v2, v0 being Element of L holds (v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" (v0 "/\" v2))) = v0 "\/" (v1 "\/" (v0 "/\" v2))

proof

let v1, v2, v0 be Element of L; :: thesis:
(v0 "\/" v1) "\/" (v0 "/\" v2) = v0 "\/" (v1 "\/" (v0 "/\" v2)) by A7;
hence (v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" (v0 "/\" v2))) = v0 "\/" (v1 "\/" (v0 "/\" v2)) by A508; :: thesis:

end;

A513: for v0, v2, v1 being Element of L holds v0 "/\" (v1 "\/" v2) = ((v1 "\/" v2) "/\" v0) "\/" (v0 "/\" v1)

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "/\" v1) "\/" ((v1 "\/" v2) "/\" v0) = v0 "/\" (v1 "\/" v2) by A131;
hence v0 "/\" (v1 "\/" v2) = ((v1 "\/" v2) "/\" v0) "\/" (v0 "/\" v1) by A8; :: thesis:

end;

A517: for v0, v1, v2 being Element of L holds (v0 "/\" v1) "\/" ((v2 "\/" v1) "/\" v0) = v0 "/\" (v1 "\/" v2)

proof

let v0, v1, v2 be Element of L; :: thesis:
v1 "\/" v2 = v2 "\/" v1 by A8;
hence (v0 "/\" v1) "\/" ((v2 "\/" v1) "/\" v0) = v0 "/\" (v1 "\/" v2) by A131; :: thesis:

end;

A520: for v101, v2, v1 being Element of L holds ((v101 "\/" v1) "/\" v101) "\/" ((v101 "\/" v1) "/\" ((v1 "/\" v2) "\/" v101)) = v101 "\/" (v1 "/\" v2)

proof

let v101, v2, v1 be Element of L; :: thesis:
(v101 "\/" v1) "/\" (v101 "\/" (v1 "/\" v2)) = v101 "\/" (v1 "/\" v2) by A11;
hence ((v101 "\/" v1) "/\" v101) "\/" ((v101 "\/" v1) "/\" ((v1 "/\" v2) "\/" v101)) = v101 "\/" (v1 "/\" v2) by A133; :: thesis:

end;

A523: for v0, v2, v1 being Element of L holds (v0 "/\" (v0 "\/" v1)) "\/" ((v0 "\/" v1) "/\" ((v1 "/\" v2) "\/" v0)) = v0 "\/" (v1 "/\" v2)

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "\/" v1) "/\" v0 = v0 "/\" (v0 "\/" v1) by A4;
hence (v0 "/\" (v0 "\/" v1)) "\/" ((v0 "\/" v1) "/\" ((v1 "/\" v2) "\/" v0)) = v0 "\/" (v1 "/\" v2) by A520; :: thesis:

end;

A525: for v0, v2, v1 being Element of L holds (v0 "/\" (v0 "\/" v1)) "\/" ((v1 "/\" v2) "\/" v0) = v0 "\/" (v1 "/\" v2)

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "\/" v1) "/\" ((v1 "/\" v2) "\/" v0) = (v1 "/\" v2) "\/" v0 by A432;
hence (v0 "/\" (v0 "\/" v1)) "\/" ((v1 "/\" v2) "\/" v0) = v0 "\/" (v1 "/\" v2) by A523; :: thesis:

end;

A527: for v0, v2, v1 being Element of L holds v0 "\/" ((v0 "/\" v1) "\/" ((v1 "/\" v2) "\/" v0)) = v0 "\/" (v1 "/\" v2)

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "/\" (v0 "\/" v1)) "\/" ((v1 "/\" v2) "\/" v0) = v0 "\/" ((v0 "/\" v1) "\/" ((v1 "/\" v2) "\/" v0)) by A403;
hence v0 "\/" ((v0 "/\" v1) "\/" ((v1 "/\" v2) "\/" v0)) = v0 "\/" (v1 "/\" v2) by A525; :: thesis:

end;

A529: for v0, v2, v1 being Element of L holds (v0 "/\" v1) "\/" ((v1 "/\" v2) "\/" v0) = v0 "\/" (v1 "/\" v2)

proof

let v0, v2, v1 be Element of L; :: thesis:
v0 "\/" ((v0 "/\" v1) "\/" ((v1 "/\" v2) "\/" v0)) = (v0 "/\" v1) "\/" ((v1 "/\" v2) "\/" v0) by A205;
hence (v0 "/\" v1) "\/" ((v1 "/\" v2) "\/" v0) = v0 "\/" (v1 "/\" v2) by A527; :: thesis:

end;

A532: for v100, v1, v102 being Element of L holds (v100 "/\" (v1 "/\" (v102 "\/" v1))) "\/" (v100 "/\" (v102 "\/" v1)) = v100 "/\" ((v1 "/\" (v102 "\/" v1)) "\/" v102)

proof

let v100, v1, v102 be Element of L; :: thesis:
v102 "\/" (v1 "/\" (v102 "\/" v1)) = v102 "\/" v1 by A386;
hence (v100 "/\" (v1 "/\" (v102 "\/" v1))) "\/" (v100 "/\" (v102 "\/" v1)) = v100 "/\" ((v1 "/\" (v102 "\/" v1)) "\/" v102) by A133; :: thesis:

end;

A535: for v0, v1, v2 being Element of L holds (v0 "/\" (v2 "\/" v1)) "\/" (v0 "/\" (v1 "/\" (v2 "\/" v1))) = v0 "/\" ((v1 "/\" (v2 "\/" v1)) "\/" v2)

proof

let v0, v1, v2 be Element of L; :: thesis:
(v0 "/\" (v1 "/\" (v2 "\/" v1))) "\/" (v0 "/\" (v2 "\/" v1)) = (v0 "/\" (v2 "\/" v1)) "\/" (v0 "/\" (v1 "/\" (v2 "\/" v1))) by A8;
hence (v0 "/\" (v2 "\/" v1)) "\/" (v0 "/\" (v1 "/\" (v2 "\/" v1))) = v0 "/\" ((v1 "/\" (v2 "\/" v1)) "\/" v2) by A532; :: thesis:

end;

A538: for v0, v2, v1 being Element of L holds v0 "/\" ((v1 "\/" v2) "/\" ((v0 "/\" (v1 "\/" v2)) "\/" v2)) = v0 "/\" ((v2 "/\" (v1 "\/" v2)) "\/" v1)

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" (v2 "/\" (v1 "\/" v2))) = v0 "/\" ((v1 "\/" v2) "/\" ((v0 "/\" (v1 "\/" v2)) "\/" v2)) by A448;
hence v0 "/\" ((v1 "\/" v2) "/\" ((v0 "/\" (v1 "\/" v2)) "\/" v2)) = v0 "/\" ((v2 "/\" (v1 "\/" v2)) "\/" v1) by A535; :: thesis:

end;

A540: for v0, v2, v1 being Element of L holds v0 "/\" ((v1 "\/" v2) "/\" (v2 "\/" (v0 "/\" (v1 "\/" v2)))) = v0 "/\" ((v2 "/\" (v1 "\/" v2)) "\/" v1)

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "/\" (v1 "\/" v2)) "\/" v2 = v2 "\/" (v0 "/\" (v1 "\/" v2)) by A8;
hence v0 "/\" ((v1 "\/" v2) "/\" (v2 "\/" (v0 "/\" (v1 "\/" v2)))) = v0 "/\" ((v2 "/\" (v1 "\/" v2)) "\/" v1) by A538; :: thesis:

end;

A542: for v0, v2, v1 being Element of L holds v0 "/\" ((v1 "\/" v2) "/\" (v2 "\/" (v0 "/\" (v1 "\/" v2)))) = v0 "/\" (v1 "\/" (v2 "/\" (v1 "\/" v2)))

proof

let v0, v2, v1 be Element of L; :: thesis:
(v2 "/\" (v1 "\/" v2)) "\/" v1 = v1 "\/" (v2 "/\" (v1 "\/" v2)) by A8;
hence v0 "/\" ((v1 "\/" v2) "/\" (v2 "\/" (v0 "/\" (v1 "\/" v2)))) = v0 "/\" (v1 "\/" (v2 "/\" (v1 "\/" v2))) by A540; :: thesis:

end;

A544: for v0, v2, v1 being Element of L holds v0 "/\" ((v1 "\/" v2) "/\" (v2 "\/" (v0 "/\" (v1 "\/" v2)))) = v0 "/\" (v1 "\/" v2)

proof

let v0, v2, v1 be Element of L; :: thesis:
v1 "\/" (v2 "/\" (v1 "\/" v2)) = v1 "\/" v2 by A386;
hence v0 "/\" ((v1 "\/" v2) "/\" (v2 "\/" (v0 "/\" (v1 "\/" v2)))) = v0 "/\" (v1 "\/" v2) by A542; :: thesis:

end;

A547: for v101, v1, v2 being Element of L holds ((v101 "\/" v1) "/\" v101) "\/" (v101 "\/" (v2 "/\" v1)) = (v101 "\/" v1) "/\" (v101 "\/" (v2 "/\" v1))

proof

let v101, v1, v2 be Element of L; :: thesis:
(v101 "\/" v1) "/\" (v101 "\/" (v2 "/\" v1)) = v101 "\/" (v2 "/\" v1) by A186;
hence ((v101 "\/" v1) "/\" v101) "\/" (v101 "\/" (v2 "/\" v1)) = (v101 "\/" v1) "/\" (v101 "\/" (v2 "/\" v1)) by A23; :: thesis:

end;

A550: for v0, v1, v2 being Element of L holds (v0 "/\" (v0 "\/" v1)) "\/" (v0 "\/" (v2 "/\" v1)) = (v0 "\/" v1) "/\" (v0 "\/" (v2 "/\" v1))

proof

let v0, v1, v2 be Element of L; :: thesis:
(v0 "\/" v1) "/\" v0 = v0 "/\" (v0 "\/" v1) by A4;
hence (v0 "/\" (v0 "\/" v1)) "\/" (v0 "\/" (v2 "/\" v1)) = (v0 "\/" v1) "/\" (v0 "\/" (v2 "/\" v1)) by A547; :: thesis:

end;

A552: for v2, v1, v0 being Element of L holds v0 "\/" ((v0 "/\" (v0 "\/" v1)) "\/" (v2 "/\" v1)) = (v0 "\/" v1) "/\" (v0 "\/" (v2 "/\" v1))

proof

let v2, v1, v0 be Element of L; :: thesis:
(v0 "/\" (v0 "\/" v1)) "\/" (v0 "\/" (v2 "/\" v1)) = v0 "\/" ((v0 "/\" (v0 "\/" v1)) "\/" (v2 "/\" v1)) by A57;
hence v0 "\/" ((v0 "/\" (v0 "\/" v1)) "\/" (v2 "/\" v1)) = (v0 "\/" v1) "/\" (v0 "\/" (v2 "/\" v1)) by A550; :: thesis:

end;

A554: for v2, v1, v0 being Element of L holds v0 "\/" (v0 "\/" ((v0 "/\" v1) "\/" (v2 "/\" v1))) = (v0 "\/" v1) "/\" (v0 "\/" (v2 "/\" v1))

proof

let v2, v1, v0 be Element of L; :: thesis:
(v0 "/\" (v0 "\/" v1)) "\/" (v2 "/\" v1) = v0 "\/" ((v0 "/\" v1) "\/" (v2 "/\" v1)) by A403;
hence v0 "\/" (v0 "\/" ((v0 "/\" v1) "\/" (v2 "/\" v1))) = (v0 "\/" v1) "/\" (v0 "\/" (v2 "/\" v1)) by A552; :: thesis:

end;

A556: for v2, v1, v0 being Element of L holds v0 "\/" ((v0 "/\" v1) "\/" (v2 "/\" v1)) = (v0 "\/" v1) "/\" (v0 "\/" (v2 "/\" v1))

proof

let v2, v1, v0 be Element of L; :: thesis:
v0 "\/" (v0 "\/" ((v0 "/\" v1) "\/" (v2 "/\" v1))) = v0 "\/" ((v0 "/\" v1) "\/" (v2 "/\" v1)) by A43;
hence v0 "\/" ((v0 "/\" v1) "\/" (v2 "/\" v1)) = (v0 "\/" v1) "/\" (v0 "\/" (v2 "/\" v1)) by A554; :: thesis:

end;

A558: for v2, v1, v0 being Element of L holds v0 "\/" ((v0 "/\" v1) "\/" (v2 "/\" v1)) = v0 "\/" (v2 "/\" v1)

proof

let v2, v1, v0 be Element of L; :: thesis:
(v0 "\/" v1) "/\" (v0 "\/" (v2 "/\" v1)) = v0 "\/" (v2 "/\" v1) by A186;
hence v0 "\/" ((v0 "/\" v1) "\/" (v2 "/\" v1)) = v0 "\/" (v2 "/\" v1) by A556; :: thesis:

end;

A561: for v102, v1, v100 being Element of L holds (v100 "\/" v1) "/\" (v100 "\/" (v102 "/\" (v100 "\/" v1))) = v100 "\/" (v102 "/\" (v100 "\/" v1))

proof

let v102, v1, v100 be Element of L; :: thesis:
v100 "\/" (v100 "\/" v1) = v100 "\/" v1 by A43;
hence (v100 "\/" v1) "/\" (v100 "\/" (v102 "/\" (v100 "\/" v1))) = v100 "\/" (v102 "/\" (v100 "\/" v1)) by A186; :: thesis:

end;

A565: for v102, v100, v1 being Element of L holds (v1 "\/" v100) "/\" (v100 "\/" (v102 "/\" (v1 "\/" v100))) = v100 "\/" (v102 "/\" (v1 "\/" v100))

proof

let v102, v100, v1 be Element of L; :: thesis:
v100 "\/" (v1 "\/" v100) = v1 "\/" v100 by A51;
hence (v1 "\/" v100) "/\" (v100 "\/" (v102 "/\" (v1 "\/" v100))) = v100 "\/" (v102 "/\" (v1 "\/" v100)) by A186; :: thesis:

end;

A568: for v0, v2, v1 being Element of L holds v0 "/\" (v1 "\/" (v0 "/\" (v1 "\/" v2))) = v0 "/\" (v1 "\/" v2)

proof

let v0, v2, v1 be Element of L; :: thesis:
(v1 "\/" v2) "/\" (v1 "\/" (v0 "/\" (v1 "\/" v2))) = v1 "\/" (v0 "/\" (v1 "\/" v2)) by A561;
hence v0 "/\" (v1 "\/" (v0 "/\" (v1 "\/" v2))) = v0 "/\" (v1 "\/" v2) by A458; :: thesis:

end;

A570: for v0, v2, v1 being Element of L holds v0 "/\" (v2 "\/" (v0 "/\" (v1 "\/" v2))) = v0 "/\" (v1 "\/" v2)

proof

let v0, v2, v1 be Element of L; :: thesis:
(v1 "\/" v2) "/\" (v2 "\/" (v0 "/\" (v1 "\/" v2))) = v2 "\/" (v0 "/\" (v1 "\/" v2)) by A565;
hence v0 "/\" (v2 "\/" (v0 "/\" (v1 "\/" v2))) = v0 "/\" (v1 "\/" v2) by A544; :: thesis:

end;

A574: for v101, v1, v2, v102 being Element of L holds (v1 "/\" ((v1 "\/" v102) "/\" v2)) "/\" (v101 "/\" (v1 "/\" (v102 "/\" v2))) = v101 "/\" (v102 "/\" (v1 "/\" ((v1 "\/" v102) "/\" v2)))

proof

let v101, v1, v2, v102 be Element of L; :: thesis:
v102 "/\" (v1 "/\" ((v1 "\/" v102) "/\" v2)) = v1 "/\" (v102 "/\" v2) by A323;
hence (v1 "/\" ((v1 "\/" v102) "/\" v2)) "/\" (v101 "/\" (v1 "/\" (v102 "/\" v2))) = v101 "/\" (v102 "/\" (v1 "/\" ((v1 "\/" v102) "/\" v2))) by A180; :: thesis:

end;

A577: for v3, v0, v2, v1 being Element of L holds v0 "/\" (((v0 "\/" v1) "/\" v2) "/\" (v3 "/\" (v0 "/\" (v1 "/\" v2)))) = v3 "/\" (v1 "/\" (v0 "/\" ((v0 "\/" v1) "/\" v2)))

proof

let v3, v0, v2, v1 be Element of L; :: thesis:
(v0 "/\" ((v0 "\/" v1) "/\" v2)) "/\" (v3 "/\" (v0 "/\" (v1 "/\" v2))) = v0 "/\" (((v0 "\/" v1) "/\" v2) "/\" (v3 "/\" (v0 "/\" (v1 "/\" v2)))) by A3;
hence v0 "/\" (((v0 "\/" v1) "/\" v2) "/\" (v3 "/\" (v0 "/\" (v1 "/\" v2)))) = v3 "/\" (v1 "/\" (v0 "/\" ((v0 "\/" v1) "/\" v2))) by A574; :: thesis:

end;

A579: for v3, v0, v2, v1 being Element of L holds v0 "/\" ((v0 "\/" v1) "/\" (v2 "/\" (v3 "/\" (v0 "/\" (v1 "/\" v2))))) = v3 "/\" (v1 "/\" (v0 "/\" ((v0 "\/" v1) "/\" v2)))

proof

let v3, v0, v2, v1 be Element of L; :: thesis:
((v0 "\/" v1) "/\" v2) "/\" (v3 "/\" (v0 "/\" (v1 "/\" v2))) = (v0 "\/" v1) "/\" (v2 "/\" (v3 "/\" (v0 "/\" (v1 "/\" v2)))) by A3;
hence v0 "/\" ((v0 "\/" v1) "/\" (v2 "/\" (v3 "/\" (v0 "/\" (v1 "/\" v2))))) = v3 "/\" (v1 "/\" (v0 "/\" ((v0 "\/" v1) "/\" v2))) by A577; :: thesis:

end;

A581: for v3, v0, v2, v1 being Element of L holds v0 "/\" ((v0 "\/" v1) "/\" (v3 "/\" (v0 "/\" (v1 "/\" v2)))) = v3 "/\" (v1 "/\" (v0 "/\" ((v0 "\/" v1) "/\" v2)))

proof

let v3, v0, v2, v1 be Element of L; :: thesis:
v2 "/\" (v3 "/\" (v0 "/\" (v1 "/\" v2))) = v3 "/\" (v0 "/\" (v1 "/\" v2)) by A470;
hence v0 "/\" ((v0 "\/" v1) "/\" (v3 "/\" (v0 "/\" (v1 "/\" v2)))) = v3 "/\" (v1 "/\" (v0 "/\" ((v0 "\/" v1) "/\" v2))) by A579; :: thesis:

end;

A584: for v2, v0, v3, v1 being Element of L holds (v0 "\/" v1) "/\" (v2 "/\" (v0 "/\" (v1 "/\" v3))) = v2 "/\" (v1 "/\" (v0 "/\" ((v0 "\/" v1) "/\" v3)))

proof

let v2, v0, v3, v1 be Element of L; :: thesis:
v0 "/\" ((v0 "\/" v1) "/\" (v2 "/\" (v0 "/\" (v1 "/\" v3)))) = (v0 "\/" v1) "/\" (v2 "/\" (v0 "/\" (v1 "/\" v3))) by A464;
hence (v0 "\/" v1) "/\" (v2 "/\" (v0 "/\" (v1 "/\" v3))) = v2 "/\" (v1 "/\" (v0 "/\" ((v0 "\/" v1) "/\" v3))) by A581; :: thesis:

end;

A586: for v2, v0, v3, v1 being Element of L holds (v0 "\/" v1) "/\" (v2 "/\" (v0 "/\" (v1 "/\" v3))) = v2 "/\" (v0 "/\" (v1 "/\" v3))

proof

let v2, v0, v3, v1 be Element of L; :: thesis:
v1 "/\" (v0 "/\" ((v0 "\/" v1) "/\" v3)) = v0 "/\" (v1 "/\" v3) by A323;
hence (v0 "\/" v1) "/\" (v2 "/\" (v0 "/\" (v1 "/\" v3))) = v2 "/\" (v0 "/\" (v1 "/\" v3)) by A584; :: thesis:

end;

A589: for v102, v1, v100 being Element of L holds v100 "/\" ((v100 "/\" (v100 "\/" v1)) "/\" ((v100 "/\" v1) "\/" v102)) = v100 "/\" ((v100 "/\" v1) "\/" v102)

proof

let v102, v1, v100 be Element of L; :: thesis:
v100 "\/" (v100 "/\" v1) = v100 "/\" (v100 "\/" v1) by A347;
hence v100 "/\" ((v100 "/\" (v100 "\/" v1)) "/\" ((v100 "/\" v1) "\/" v102)) = v100 "/\" ((v100 "/\" v1) "\/" v102) by A351; :: thesis:

end;

A592: for v2, v1, v0 being Element of L holds v0 "/\" (v0 "/\" ((v0 "\/" v1) "/\" ((v0 "/\" v1) "\/" v2))) = v0 "/\" ((v0 "/\" v1) "\/" v2)

proof

let v2, v1, v0 be Element of L; :: thesis:
(v0 "/\" (v0 "\/" v1)) "/\" ((v0 "/\" v1) "\/" v2) = v0 "/\" ((v0 "\/" v1) "/\" ((v0 "/\" v1) "\/" v2)) by A3;
hence v0 "/\" (v0 "/\" ((v0 "\/" v1) "/\" ((v0 "/\" v1) "\/" v2))) = v0 "/\" ((v0 "/\" v1) "\/" v2) by A589; :: thesis:

end;

A594: for v2, v1, v0 being Element of L holds v0 "/\" ((v0 "\/" v1) "/\" ((v0 "/\" v1) "\/" v2)) = v0 "/\" ((v0 "/\" v1) "\/" v2)

proof

let v2, v1, v0 be Element of L; :: thesis:
v0 "/\" (v0 "/\" ((v0 "\/" v1) "/\" ((v0 "/\" v1) "\/" v2))) = v0 "/\" ((v0 "\/" v1) "/\" ((v0 "/\" v1) "\/" v2)) by A26;
hence v0 "/\" ((v0 "\/" v1) "/\" ((v0 "/\" v1) "\/" v2)) = v0 "/\" ((v0 "/\" v1) "\/" v2) by A592; :: thesis:

end;

A597: for v100, v1, v2, v101 being Element of L holds v100 "/\" ((v100 "\/" v101) "/\" (v1 "\/" (v101 "\/" v2))) = v100 "/\" (v101 "\/" (v1 "\/" (v101 "\/" v2)))

proof

let v100, v1, v2, v101 be Element of L; :: thesis:
v101 "\/" (v1 "\/" (v101 "\/" v2)) = v1 "\/" (v101 "\/" v2) by A195;
hence v100 "/\" ((v100 "\/" v101) "/\" (v1 "\/" (v101 "\/" v2))) = v100 "/\" (v101 "\/" (v1 "\/" (v101 "\/" v2))) by A351; :: thesis:

end;

A600: for v0, v2, v3, v1 being Element of L holds v0 "/\" ((v0 "\/" v1) "/\" (v2 "\/" (v1 "\/" v3))) = v0 "/\" (v2 "\/" (v1 "\/" v3))

proof

let v0, v2, v3, v1 be Element of L; :: thesis:
v1 "\/" (v2 "\/" (v1 "\/" v3)) = v2 "\/" (v1 "\/" v3) by A195;
hence v0 "/\" ((v0 "\/" v1) "/\" (v2 "\/" (v1 "\/" v3))) = v0 "/\" (v2 "\/" (v1 "\/" v3)) by A597; :: thesis:

end;

A603: for v101, v1, v0 being Element of L holds v0 "\/" ((v0 "/\" v1) "\/" v101) = v101 "\/" (v0 "/\" (v0 "\/" v1))

proof

let v101, v1, v0 be Element of L; :: thesis:
(v0 "/\" (v0 "\/" v1)) "\/" v101 = v0 "\/" ((v0 "/\" v1) "\/" v101) by A403;
hence v0 "\/" ((v0 "/\" v1) "\/" v101) = v101 "\/" (v0 "/\" (v0 "\/" v1)) by A8; :: thesis:

end;

A607: for v101, v1, v0 being Element of L holds v0 "\/" ((v0 "/\" v1) "\/" ((v0 "/\" (v0 "\/" v1)) "/\" v101)) = (v0 "/\" (v0 "\/" v1)) "/\" ((v0 "/\" (v0 "\/" v1)) "\/" v101)

proof

let v101, v1, v0 be Element of L; :: thesis:
(v0 "/\" (v0 "\/" v1)) "\/" ((v0 "/\" (v0 "\/" v1)) "/\" v101) = v0 "\/" ((v0 "/\" v1) "\/" ((v0 "/\" (v0 "\/" v1)) "/\" v101)) by A403;
hence v0 "\/" ((v0 "/\" v1) "\/" ((v0 "/\" (v0 "\/" v1)) "/\" v101)) = (v0 "/\" (v0 "\/" v1)) "/\" ((v0 "/\" (v0 "\/" v1)) "\/" v101) by A347; :: thesis:

end;

A610: for v2, v1, v0 being Element of L holds v0 "\/" ((v0 "/\" v1) "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) = (v0 "/\" (v0 "\/" v1)) "/\" ((v0 "/\" (v0 "\/" v1)) "\/" v2)

proof

let v2, v1, v0 be Element of L; :: thesis:
(v0 "/\" (v0 "\/" v1)) "/\" v2 = v0 "/\" ((v0 "\/" v1) "/\" v2) by A3;
hence v0 "\/" ((v0 "/\" v1) "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) = (v0 "/\" (v0 "\/" v1)) "/\" ((v0 "/\" (v0 "\/" v1)) "\/" v2) by A607; :: thesis:

end;

A612: for v2, v1, v0 being Element of L holds v0 "\/" ((v0 "/\" v1) "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) = (v0 "/\" (v0 "\/" v1)) "/\" (v0 "\/" ((v0 "/\" v1) "\/" v2))

proof

let v2, v1, v0 be Element of L; :: thesis:
(v0 "/\" (v0 "\/" v1)) "\/" v2 = v0 "\/" ((v0 "/\" v1) "\/" v2) by A403;
hence v0 "\/" ((v0 "/\" v1) "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) = (v0 "/\" (v0 "\/" v1)) "/\" (v0 "\/" ((v0 "/\" v1) "\/" v2)) by A610; :: thesis:

end;

A614: for v2, v1, v0 being Element of L holds v0 "\/" ((v0 "/\" v1) "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) = v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" ((v0 "/\" v1) "\/" v2)))

proof

let v2, v1, v0 be Element of L; :: thesis:
(v0 "/\" (v0 "\/" v1)) "/\" (v0 "\/" ((v0 "/\" v1) "\/" v2)) = v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" ((v0 "/\" v1) "\/" v2))) by A3;
hence v0 "\/" ((v0 "/\" v1) "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) = v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" ((v0 "/\" v1) "\/" v2))) by A612; :: thesis:

end;

A617: for v101, v1, v0 being Element of L holds v0 "\/" ((v0 "/\" v1) "\/" (v101 "/\" (v0 "/\" (v0 "\/" v1)))) = (v0 "/\" (v0 "\/" v1)) "/\" ((v0 "/\" (v0 "\/" v1)) "\/" v101)

proof

let v101, v1, v0 be Element of L; :: thesis:
(v0 "/\" (v0 "\/" v1)) "\/" (v101 "/\" (v0 "/\" (v0 "\/" v1))) = v0 "\/" ((v0 "/\" v1) "\/" (v101 "/\" (v0 "/\" (v0 "\/" v1)))) by A403;
hence v0 "\/" ((v0 "/\" v1) "\/" (v101 "/\" (v0 "/\" (v0 "\/" v1)))) = (v0 "/\" (v0 "\/" v1)) "/\" ((v0 "/\" (v0 "\/" v1)) "\/" v101) by A400; :: thesis:

end;

A620: for v2, v1, v0 being Element of L holds v0 "\/" ((v0 "/\" v1) "\/" (v2 "/\" (v0 "/\" (v0 "\/" v1)))) = (v0 "/\" (v0 "\/" v1)) "/\" (v0 "\/" ((v0 "/\" v1) "\/" v2))

proof

let v2, v1, v0 be Element of L; :: thesis:
(v0 "/\" (v0 "\/" v1)) "\/" v2 = v0 "\/" ((v0 "/\" v1) "\/" v2) by A403;
hence v0 "\/" ((v0 "/\" v1) "\/" (v2 "/\" (v0 "/\" (v0 "\/" v1)))) = (v0 "/\" (v0 "\/" v1)) "/\" (v0 "\/" ((v0 "/\" v1) "\/" v2)) by A617; :: thesis:

end;

A622: for v2, v1, v0 being Element of L holds v0 "\/" ((v0 "/\" v1) "\/" (v2 "/\" (v0 "/\" (v0 "\/" v1)))) = v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" ((v0 "/\" v1) "\/" v2)))

proof

let v2, v1, v0 be Element of L; :: thesis:
(v0 "/\" (v0 "\/" v1)) "/\" (v0 "\/" ((v0 "/\" v1) "\/" v2)) = v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" ((v0 "/\" v1) "\/" v2))) by A3;
hence v0 "\/" ((v0 "/\" v1) "\/" (v2 "/\" (v0 "/\" (v0 "\/" v1)))) = v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" ((v0 "/\" v1) "\/" v2))) by A620; :: thesis:

end;

A625: for v101, v0, v102, v1 being Element of L holds (v0 "/\" v1) "\/" (v101 "/\" (v0 "/\" (v1 "/\" v102))) = (v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" (v101 "/\" v102))

proof

let v101, v0, v102, v1 be Element of L; :: thesis:
(v0 "/\" v1) "/\" v102 = v0 "/\" (v1 "/\" v102) by A3;
hence (v0 "/\" v1) "\/" (v101 "/\" (v0 "/\" (v1 "/\" v102))) = (v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" (v101 "/\" v102)) by A417; :: thesis:

end;

A628: for v2, v0, v3, v1 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" (v0 "/\" (v1 "/\" v3))) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" (v2 "/\" v3)))

proof

let v2, v0, v3, v1 be Element of L; :: thesis:
(v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" (v2 "/\" v3)) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" (v2 "/\" v3))) by A3;
hence (v0 "/\" v1) "\/" (v2 "/\" (v0 "/\" (v1 "/\" v3))) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" (v2 "/\" v3))) by A625; :: thesis:

end;

A631: for v0, v1, v102, v100 being Element of L holds v100 "\/" (v0 "/\" (v1 "/\" (v100 "/\" v102))) = v100 "/\" (v100 "\/" ((v0 "/\" v1) "/\" v102))

proof

let v0, v1, v102, v100 be Element of L; :: thesis:
(v0 "/\" v1) "/\" (v100 "/\" v102) = v0 "/\" (v1 "/\" (v100 "/\" v102)) by A3;
hence v100 "\/" (v0 "/\" (v1 "/\" (v100 "/\" v102))) = v100 "/\" (v100 "\/" ((v0 "/\" v1) "/\" v102)) by A417; :: thesis:

end;

A634: for v1, v2, v3, v0 being Element of L holds v0 "\/" (v1 "/\" (v2 "/\" (v0 "/\" v3))) = v0 "/\" (v0 "\/" (v1 "/\" (v2 "/\" v3)))

proof

let v1, v2, v3, v0 be Element of L; :: thesis:
(v1 "/\" v2) "/\" v3 = v1 "/\" (v2 "/\" v3) by A3;
hence v0 "\/" (v1 "/\" (v2 "/\" (v0 "/\" v3))) = v0 "/\" (v0 "\/" (v1 "/\" (v2 "/\" v3))) by A631; :: thesis:

end;

A637: for v1, v2, v102, v101 being Element of L holds ((v1 "/\" ((v101 "/\" v102) "/\" v2)) "/\" v101) "\/" (v102 "/\" ((v101 "/\" v102) "/\" ((v101 "/\" v102) "\/" (v1 "/\" v2)))) = (v102 "\/" ((v101 "\/" v102) "/\" (v1 "/\" ((v101 "/\" v102) "/\" v2)))) "/\" ((v1 "/\" ((v101 "/\" v102) "/\" v2)) "\/" v101)

proof

let v1, v2, v102, v101 be Element of L; :: thesis:
(v101 "/\" v102) "\/" (v1 "/\" ((v101 "/\" v102) "/\" v2)) = (v101 "/\" v102) "/\" ((v101 "/\" v102) "\/" (v1 "/\" v2)) by A417;
hence ((v1 "/\" ((v101 "/\" v102) "/\" v2)) "/\" v101) "\/" (v102 "/\" ((v101 "/\" v102) "/\" ((v101 "/\" v102) "\/" (v1 "/\" v2)))) = (v102 "\/" ((v101 "\/" v102) "/\" (v1 "/\" ((v101 "/\" v102) "/\" v2)))) "/\" ((v1 "/\" ((v101 "/\" v102) "/\" v2)) "\/" v101) by A20; :: thesis:

end;

A640: for v0, v1, v3, v2 being Element of L holds ((v0 "/\" (v1 "/\" (v2 "/\" v3))) "/\" v1) "\/" (v2 "/\" ((v1 "/\" v2) "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3)))) = (v2 "\/" ((v1 "\/" v2) "/\" (v0 "/\" ((v1 "/\" v2) "/\" v3)))) "/\" ((v0 "/\" ((v1 "/\" v2) "/\" v3)) "\/" v1)

proof

let v0, v1, v3, v2 be Element of L; :: thesis:
(v1 "/\" v2) "/\" v3 = v1 "/\" (v2 "/\" v3) by A3;
hence ((v0 "/\" (v1 "/\" (v2 "/\" v3))) "/\" v1) "\/" (v2 "/\" ((v1 "/\" v2) "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3)))) = (v2 "\/" ((v1 "\/" v2) "/\" (v0 "/\" ((v1 "/\" v2) "/\" v3)))) "/\" ((v0 "/\" ((v1 "/\" v2) "/\" v3)) "\/" v1) by A637; :: thesis:

end;

A642: for v0, v1, v3, v2 being Element of L holds (v1 "/\" (v0 "/\" (v1 "/\" (v2 "/\" v3)))) "\/" (v2 "/\" ((v1 "/\" v2) "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3)))) = (v2 "\/" ((v1 "\/" v2) "/\" (v0 "/\" ((v1 "/\" v2) "/\" v3)))) "/\" ((v0 "/\" ((v1 "/\" v2) "/\" v3)) "\/" v1)

proof

let v0, v1, v3, v2 be Element of L; :: thesis:
(v0 "/\" (v1 "/\" (v2 "/\" v3))) "/\" v1 = v1 "/\" (v0 "/\" (v1 "/\" (v2 "/\" v3))) by A4;
hence (v1 "/\" (v0 "/\" (v1 "/\" (v2 "/\" v3)))) "\/" (v2 "/\" ((v1 "/\" v2) "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3)))) = (v2 "\/" ((v1 "\/" v2) "/\" (v0 "/\" ((v1 "/\" v2) "/\" v3)))) "/\" ((v0 "/\" ((v1 "/\" v2) "/\" v3)) "\/" v1) by A640; :: thesis:

end;

A645: for v1, v0, v3, v2 being Element of L holds (v1 "/\" (v0 "/\" (v2 "/\" v3))) "\/" (v2 "/\" ((v0 "/\" v2) "/\" ((v0 "/\" v2) "\/" (v1 "/\" v3)))) = (v2 "\/" ((v0 "\/" v2) "/\" (v1 "/\" ((v0 "/\" v2) "/\" v3)))) "/\" ((v1 "/\" ((v0 "/\" v2) "/\" v3)) "\/" v0)

proof

let v1, v0, v3, v2 be Element of L; :: thesis:
v0 "/\" (v1 "/\" (v0 "/\" (v2 "/\" v3))) = v1 "/\" (v0 "/\" (v2 "/\" v3)) by A162;
hence (v1 "/\" (v0 "/\" (v2 "/\" v3))) "\/" (v2 "/\" ((v0 "/\" v2) "/\" ((v0 "/\" v2) "\/" (v1 "/\" v3)))) = (v2 "\/" ((v0 "\/" v2) "/\" (v1 "/\" ((v0 "/\" v2) "/\" v3)))) "/\" ((v1 "/\" ((v0 "/\" v2) "/\" v3)) "\/" v0) by A642; :: thesis:

end;

A648: for v0, v1, v3, v2 being Element of L holds (v0 "/\" (v1 "/\" (v2 "/\" v3))) "\/" (v2 "/\" (v1 "/\" (v2 "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3))))) = (v2 "\/" ((v1 "\/" v2) "/\" (v0 "/\" ((v1 "/\" v2) "/\" v3)))) "/\" ((v0 "/\" ((v1 "/\" v2) "/\" v3)) "\/" v1)

proof

let v0, v1, v3, v2 be Element of L; :: thesis:
(v1 "/\" v2) "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3)) = v1 "/\" (v2 "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3))) by A3;
hence (v0 "/\" (v1 "/\" (v2 "/\" v3))) "\/" (v2 "/\" (v1 "/\" (v2 "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3))))) = (v2 "\/" ((v1 "\/" v2) "/\" (v0 "/\" ((v1 "/\" v2) "/\" v3)))) "/\" ((v0 "/\" ((v1 "/\" v2) "/\" v3)) "\/" v1) by A645; :: thesis:

end;

A650: for v0, v1, v3, v2 being Element of L holds (v0 "/\" (v1 "/\" (v2 "/\" v3))) "\/" (v1 "/\" (v2 "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3)))) = (v2 "\/" ((v1 "\/" v2) "/\" (v0 "/\" ((v1 "/\" v2) "/\" v3)))) "/\" ((v0 "/\" ((v1 "/\" v2) "/\" v3)) "\/" v1)

proof

let v0, v1, v3, v2 be Element of L; :: thesis:
v2 "/\" (v1 "/\" (v2 "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3)))) = v1 "/\" (v2 "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3))) by A162;
hence (v0 "/\" (v1 "/\" (v2 "/\" v3))) "\/" (v1 "/\" (v2 "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3)))) = (v2 "\/" ((v1 "\/" v2) "/\" (v0 "/\" ((v1 "/\" v2) "/\" v3)))) "/\" ((v0 "/\" ((v1 "/\" v2) "/\" v3)) "\/" v1) by A648; :: thesis:

end;

A652: for v0, v1, v3, v2 being Element of L holds (v0 "/\" (v1 "/\" (v2 "/\" v3))) "\/" (v1 "/\" (v2 "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3)))) = (v2 "\/" ((v1 "\/" v2) "/\" (v0 "/\" (v1 "/\" (v2 "/\" v3))))) "/\" ((v0 "/\" ((v1 "/\" v2) "/\" v3)) "\/" v1)

proof

let v0, v1, v3, v2 be Element of L; :: thesis:
(v1 "/\" v2) "/\" v3 = v1 "/\" (v2 "/\" v3) by A3;
hence (v0 "/\" (v1 "/\" (v2 "/\" v3))) "\/" (v1 "/\" (v2 "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3)))) = (v2 "\/" ((v1 "\/" v2) "/\" (v0 "/\" (v1 "/\" (v2 "/\" v3))))) "/\" ((v0 "/\" ((v1 "/\" v2) "/\" v3)) "\/" v1) by A650; :: thesis:

end;

A654: for v0, v1, v3, v2 being Element of L holds (v0 "/\" (v1 "/\" (v2 "/\" v3))) "\/" (v1 "/\" (v2 "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3)))) = (v2 "\/" (v0 "/\" (v1 "/\" (v2 "/\" v3)))) "/\" ((v0 "/\" ((v1 "/\" v2) "/\" v3)) "\/" v1)

proof

let v0, v1, v3, v2 be Element of L; :: thesis:
(v1 "\/" v2) "/\" (v0 "/\" (v1 "/\" (v2 "/\" v3))) = v0 "/\" (v1 "/\" (v2 "/\" v3)) by A586;
hence (v0 "/\" (v1 "/\" (v2 "/\" v3))) "\/" (v1 "/\" (v2 "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3)))) = (v2 "\/" (v0 "/\" (v1 "/\" (v2 "/\" v3)))) "/\" ((v0 "/\" ((v1 "/\" v2) "/\" v3)) "\/" v1) by A652; :: thesis:

end;

A656: for v0, v1, v3, v2 being Element of L holds (v0 "/\" (v1 "/\" (v2 "/\" v3))) "\/" (v1 "/\" (v2 "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3)))) = (v2 "/\" (v2 "\/" (v0 "/\" (v1 "/\" v3)))) "/\" ((v0 "/\" ((v1 "/\" v2) "/\" v3)) "\/" v1)

proof

let v0, v1, v3, v2 be Element of L; :: thesis:
v2 "\/" (v0 "/\" (v1 "/\" (v2 "/\" v3))) = v2 "/\" (v2 "\/" (v0 "/\" (v1 "/\" v3))) by A634;
hence (v0 "/\" (v1 "/\" (v2 "/\" v3))) "\/" (v1 "/\" (v2 "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3)))) = (v2 "/\" (v2 "\/" (v0 "/\" (v1 "/\" v3)))) "/\" ((v0 "/\" ((v1 "/\" v2) "/\" v3)) "\/" v1) by A654; :: thesis:

end;

A658: for v0, v1, v3, v2 being Element of L holds (v0 "/\" (v1 "/\" (v2 "/\" v3))) "\/" (v1 "/\" (v2 "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3)))) = (v2 "/\" (v2 "\/" (v0 "/\" (v1 "/\" v3)))) "/\" ((v0 "/\" (v1 "/\" (v2 "/\" v3))) "\/" v1)

proof

let v0, v1, v3, v2 be Element of L; :: thesis:
(v1 "/\" v2) "/\" v3 = v1 "/\" (v2 "/\" v3) by A3;
hence (v0 "/\" (v1 "/\" (v2 "/\" v3))) "\/" (v1 "/\" (v2 "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3)))) = (v2 "/\" (v2 "\/" (v0 "/\" (v1 "/\" v3)))) "/\" ((v0 "/\" (v1 "/\" (v2 "/\" v3))) "\/" v1) by A656; :: thesis:

end;

A660: for v0, v1, v3, v2 being Element of L holds (v0 "/\" (v1 "/\" (v2 "/\" v3))) "\/" (v1 "/\" (v2 "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3)))) = (v2 "/\" (v2 "\/" (v0 "/\" (v1 "/\" v3)))) "/\" (v1 "\/" (v0 "/\" (v1 "/\" (v2 "/\" v3))))

proof

let v0, v1, v3, v2 be Element of L; :: thesis:
(v0 "/\" (v1 "/\" (v2 "/\" v3))) "\/" v1 = v1 "\/" (v0 "/\" (v1 "/\" (v2 "/\" v3))) by A8;
hence (v0 "/\" (v1 "/\" (v2 "/\" v3))) "\/" (v1 "/\" (v2 "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3)))) = (v2 "/\" (v2 "\/" (v0 "/\" (v1 "/\" v3)))) "/\" (v1 "\/" (v0 "/\" (v1 "/\" (v2 "/\" v3)))) by A658; :: thesis:

end;

A662: for v0, v1, v3, v2 being Element of L holds (v0 "/\" (v1 "/\" (v2 "/\" v3))) "\/" (v1 "/\" (v2 "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3)))) = (v2 "/\" (v2 "\/" (v0 "/\" (v1 "/\" v3)))) "/\" (v1 "/\" (v1 "\/" (v0 "/\" (v2 "/\" v3))))

proof

let v0, v1, v3, v2 be Element of L; :: thesis:
v1 "\/" (v0 "/\" (v1 "/\" (v2 "/\" v3))) = v1 "/\" (v1 "\/" (v0 "/\" (v2 "/\" v3))) by A417;
hence (v0 "/\" (v1 "/\" (v2 "/\" v3))) "\/" (v1 "/\" (v2 "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3)))) = (v2 "/\" (v2 "\/" (v0 "/\" (v1 "/\" v3)))) "/\" (v1 "/\" (v1 "\/" (v0 "/\" (v2 "/\" v3)))) by A660; :: thesis:

end;

A664: for v0, v1, v3, v2 being Element of L holds (v0 "/\" (v1 "/\" (v2 "/\" v3))) "\/" (v1 "/\" (v2 "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3)))) = v1 "/\" ((v2 "/\" (v2 "\/" (v0 "/\" (v1 "/\" v3)))) "/\" (v1 "\/" (v0 "/\" (v2 "/\" v3))))

proof

let v0, v1, v3, v2 be Element of L; :: thesis:
(v2 "/\" (v2 "\/" (v0 "/\" (v1 "/\" v3)))) "/\" (v1 "/\" (v1 "\/" (v0 "/\" (v2 "/\" v3)))) = v1 "/\" ((v2 "/\" (v2 "\/" (v0 "/\" (v1 "/\" v3)))) "/\" (v1 "\/" (v0 "/\" (v2 "/\" v3)))) by A40;
hence (v0 "/\" (v1 "/\" (v2 "/\" v3))) "\/" (v1 "/\" (v2 "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3)))) = v1 "/\" ((v2 "/\" (v2 "\/" (v0 "/\" (v1 "/\" v3)))) "/\" (v1 "\/" (v0 "/\" (v2 "/\" v3)))) by A662; :: thesis:

end;

A666: for v0, v1, v3, v2 being Element of L holds (v0 "/\" (v1 "/\" (v2 "/\" v3))) "\/" (v1 "/\" (v2 "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3)))) = v1 "/\" (v2 "/\" ((v2 "\/" (v0 "/\" (v1 "/\" v3))) "/\" (v1 "\/" (v0 "/\" (v2 "/\" v3)))))

proof

let v0, v1, v3, v2 be Element of L; :: thesis:
(v2 "/\" (v2 "\/" (v0 "/\" (v1 "/\" v3)))) "/\" (v1 "\/" (v0 "/\" (v2 "/\" v3))) = v2 "/\" ((v2 "\/" (v0 "/\" (v1 "/\" v3))) "/\" (v1 "\/" (v0 "/\" (v2 "/\" v3)))) by A3;
hence (v0 "/\" (v1 "/\" (v2 "/\" v3))) "\/" (v1 "/\" (v2 "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3)))) = v1 "/\" (v2 "/\" ((v2 "\/" (v0 "/\" (v1 "/\" v3))) "/\" (v1 "\/" (v0 "/\" (v2 "/\" v3))))) by A664; :: thesis:

end;

A669: for v0, v100, v1 being Element of L holds v100 "\/" ((v100 "\/" ((v1 "\/" v100) "/\" v0)) "/\" (v0 "\/" v1)) = (v0 "/\" v1) "\/" (v100 "/\" (v100 "\/" ((v1 "/\" v100) "\/" v0)))

proof

let v0, v100, v1 be Element of L; :: thesis:
(v0 "/\" v1) "\/" (v100 "/\" ((v1 "/\" v100) "\/" v0)) = (v100 "\/" ((v1 "\/" v100) "/\" v0)) "/\" (v0 "\/" v1) by A20;
hence v100 "\/" ((v100 "\/" ((v1 "\/" v100) "/\" v0)) "/\" (v0 "\/" v1)) = (v0 "/\" v1) "\/" (v100 "/\" (v100 "\/" ((v1 "/\" v100) "\/" v0))) by A421; :: thesis:

end;

A675: for v101, v1, v2, v100 being Element of L holds (v100 "/\" v101) "\/" (v101 "/\" (v1 "\/" (v100 "/\" (v100 "\/" v2)))) = v101 "/\" (v100 "\/" (v1 "\/" (v100 "/\" v2)))

proof

let v101, v1, v2, v100 be Element of L; :: thesis:
v100 "\/" (v1 "\/" (v100 "/\" v2)) = v1 "\/" (v100 "/\" (v100 "\/" v2)) by A421;
hence (v100 "/\" v101) "\/" (v101 "/\" (v1 "\/" (v100 "/\" (v100 "\/" v2)))) = v101 "/\" (v100 "\/" (v1 "\/" (v100 "/\" v2))) by A128; :: thesis:

end;

A679: for v101, v2, v100 being Element of L holds (v2 "\/" ((v100 "\/" v2) "/\" (v100 "\/" v101))) "/\" ((v100 "\/" v101) "\/" v100) = v100 "\/" ((v100 "/\" v101) "\/" (v2 "/\" ((v100 "/\" v2) "\/" (v100 "\/" v101))))

proof

let v101, v2, v100 be Element of L; :: thesis:
(v100 "/\" (v100 "\/" v101)) "\/" (v2 "/\" ((v100 "/\" v2) "\/" (v100 "\/" v101))) = (v2 "\/" ((v100 "\/" v2) "/\" (v100 "\/" v101))) "/\" ((v100 "\/" v101) "\/" v100) by A101;
hence (v2 "\/" ((v100 "\/" v2) "/\" (v100 "\/" v101))) "/\" ((v100 "\/" v101) "\/" v100) = v100 "\/" ((v100 "/\" v101) "\/" (v2 "/\" ((v100 "/\" v2) "\/" (v100 "\/" v101)))) by A403; :: thesis:

end;

A682: for v2, v0, v1 being Element of L holds (v0 "\/" ((v1 "\/" v0) "/\" (v1 "\/" v2))) "/\" (v1 "\/" (v1 "\/" v2)) = v1 "\/" ((v1 "/\" v2) "\/" (v0 "/\" ((v1 "/\" v0) "\/" (v1 "\/" v2))))

proof

let v2, v0, v1 be Element of L; :: thesis:
(v1 "\/" v2) "\/" v1 = v1 "\/" (v1 "\/" v2) by A8;
hence (v0 "\/" ((v1 "\/" v0) "/\" (v1 "\/" v2))) "/\" (v1 "\/" (v1 "\/" v2)) = v1 "\/" ((v1 "/\" v2) "\/" (v0 "/\" ((v1 "/\" v0) "\/" (v1 "\/" v2)))) by A679; :: thesis:

end;

A684: for v2, v0, v1 being Element of L holds (v0 "\/" ((v1 "\/" v0) "/\" (v1 "\/" v2))) "/\" (v1 "\/" v2) = v1 "\/" ((v1 "/\" v2) "\/" (v0 "/\" ((v1 "/\" v0) "\/" (v1 "\/" v2))))

proof

let v2, v0, v1 be Element of L; :: thesis:
v1 "\/" (v1 "\/" v2) = v1 "\/" v2 by A43;
hence (v0 "\/" ((v1 "\/" v0) "/\" (v1 "\/" v2))) "/\" (v1 "\/" v2) = v1 "\/" ((v1 "/\" v2) "\/" (v0 "/\" ((v1 "/\" v0) "\/" (v1 "\/" v2)))) by A682; :: thesis:

end;

A686: for v2, v0, v1 being Element of L holds (v1 "\/" v2) "/\" (v0 "\/" ((v1 "\/" v0) "/\" (v1 "\/" v2))) = v1 "\/" ((v1 "/\" v2) "\/" (v0 "/\" ((v1 "/\" v0) "\/" (v1 "\/" v2))))

proof

let v2, v0, v1 be Element of L; :: thesis:
(v0 "\/" ((v1 "\/" v0) "/\" (v1 "\/" v2))) "/\" (v1 "\/" v2) = (v1 "\/" v2) "/\" (v0 "\/" ((v1 "\/" v0) "/\" (v1 "\/" v2))) by A4;
hence (v1 "\/" v2) "/\" (v0 "\/" ((v1 "\/" v0) "/\" (v1 "\/" v2))) = v1 "\/" ((v1 "/\" v2) "\/" (v0 "/\" ((v1 "/\" v0) "\/" (v1 "\/" v2)))) by A684; :: thesis:

end;

A689: for v1, v2, v0 being Element of L holds (v0 "\/" v1) "/\" (v2 "\/" ((v0 "\/" v2) "/\" (v0 "\/" v1))) = v0 "\/" ((v0 "/\" v1) "\/" (v2 "/\" (v0 "\/" ((v0 "/\" v2) "\/" v1))))

proof

let v1, v2, v0 be Element of L; :: thesis:
(v0 "/\" v2) "\/" (v0 "\/" v1) = v0 "\/" ((v0 "/\" v2) "\/" v1) by A57;
hence (v0 "\/" v1) "/\" (v2 "\/" ((v0 "\/" v2) "/\" (v0 "\/" v1))) = v0 "\/" ((v0 "/\" v1) "\/" (v2 "/\" (v0 "\/" ((v0 "/\" v2) "\/" v1)))) by A686; :: thesis:

end;

A693: for v102, v1, v100 being Element of L holds v100 "\/" (v100 "\/" ((v100 "/\" v1) "\/" ((v100 "\/" v1) "/\" v102))) = v100 "\/" ((v100 "\/" v1) "/\" v102)

proof

let v102, v1, v100 be Element of L; :: thesis:
(v100 "/\" (v100 "\/" v1)) "\/" ((v100 "\/" v1) "/\" v102) = v100 "\/" ((v100 "/\" v1) "\/" ((v100 "\/" v1) "/\" v102)) by A403;
hence v100 "\/" (v100 "\/" ((v100 "/\" v1) "\/" ((v100 "\/" v1) "/\" v102))) = v100 "\/" ((v100 "\/" v1) "/\" v102) by A426; :: thesis:

end;

A696: for v2, v1, v0 being Element of L holds v0 "\/" ((v0 "/\" v1) "\/" ((v0 "\/" v1) "/\" v2)) = v0 "\/" ((v0 "\/" v1) "/\" v2)

proof

let v2, v1, v0 be Element of L; :: thesis:
v0 "\/" (v0 "\/" ((v0 "/\" v1) "\/" ((v0 "\/" v1) "/\" v2))) = v0 "\/" ((v0 "/\" v1) "\/" ((v0 "\/" v1) "/\" v2)) by A43;
hence v0 "\/" ((v0 "/\" v1) "\/" ((v0 "\/" v1) "/\" v2)) = v0 "\/" ((v0 "\/" v1) "/\" v2) by A693; :: thesis:

end;

A699: for v100, v1, v102 being Element of L holds (v100 "/\" (v102 "\/" v1)) "\/" (v102 "/\" (v102 "\/" ((v102 "/\" v1) "\/" v100))) = (v102 "\/" (((v102 "\/" v1) "\/" v102) "/\" v100)) "/\" (v100 "\/" (v102 "\/" v1))

proof

let v100, v1, v102 be Element of L; :: thesis:
(v102 "/\" (v102 "\/" v1)) "\/" v100 = v102 "\/" ((v102 "/\" v1) "\/" v100) by A403;
hence (v100 "/\" (v102 "\/" v1)) "\/" (v102 "/\" (v102 "\/" ((v102 "/\" v1) "\/" v100))) = (v102 "\/" (((v102 "\/" v1) "\/" v102) "/\" v100)) "/\" (v100 "\/" (v102 "\/" v1)) by A104; :: thesis:

end;

A702: for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v1 "/\" (v1 "\/" ((v1 "/\" v2) "\/" v0))) = (v1 "\/" ((v1 "\/" (v1 "\/" v2)) "/\" v0)) "/\" (v0 "\/" (v1 "\/" v2))

proof

let v0, v2, v1 be Element of L; :: thesis:
(v1 "\/" v2) "\/" v1 = v1 "\/" (v1 "\/" v2) by A8;
hence (v0 "/\" (v1 "\/" v2)) "\/" (v1 "/\" (v1 "\/" ((v1 "/\" v2) "\/" v0))) = (v1 "\/" ((v1 "\/" (v1 "\/" v2)) "/\" v0)) "/\" (v0 "\/" (v1 "\/" v2)) by A699; :: thesis:

end;

A704: for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v1 "/\" (v1 "\/" ((v1 "/\" v2) "\/" v0))) = (v1 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v0 "\/" (v1 "\/" v2))

proof

let v0, v2, v1 be Element of L; :: thesis:
v1 "\/" (v1 "\/" v2) = v1 "\/" v2 by A43;
hence (v0 "/\" (v1 "\/" v2)) "\/" (v1 "/\" (v1 "\/" ((v1 "/\" v2) "\/" v0))) = (v1 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v0 "\/" (v1 "\/" v2)) by A702; :: thesis:

end;

A707: for v102, v2, v101 being Element of L holds (v101 "/\" v2) "\/" (v102 "/\" (v101 "/\" v2)) = (v101 "/\" v2) "/\" ((v101 "/\" v2) "\/" (v101 "/\" v102))

proof

let v102, v2, v101 be Element of L; :: thesis:
v101 "/\" (v102 "/\" (v101 "/\" v2)) = v102 "/\" (v101 "/\" v2) by A162;
hence (v101 "/\" v2) "\/" (v102 "/\" (v101 "/\" v2)) = (v101 "/\" v2) "/\" ((v101 "/\" v2) "\/" (v101 "/\" v102)) by A441; :: thesis:

end;

A710: for v2, v1, v0 being Element of L holds (v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" v2) = (v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" (v0 "/\" v2))

proof

let v2, v1, v0 be Element of L; :: thesis:
(v0 "/\" v1) "\/" (v2 "/\" (v0 "/\" v1)) = (v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" v2) by A400;
hence (v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" v2) = (v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" (v0 "/\" v2)) by A707; :: thesis:

end;

A712: for v2, v1, v0 being Element of L holds v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2)) = (v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" (v0 "/\" v2))

proof

let v2, v1, v0 be Element of L; :: thesis:
(v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" v2) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2)) by A3;
hence v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2)) = (v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" (v0 "/\" v2)) by A710; :: thesis:

end;

A714: for v2, v1, v0 being Element of L holds v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2)) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" (v0 "/\" v2)))

proof

let v2, v1, v0 be Element of L; :: thesis:
(v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" (v0 "/\" v2)) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" (v0 "/\" v2))) by A3;
hence v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2)) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" (v0 "/\" v2))) by A712; :: thesis:

end;

A717: for v2, v1, v0 being Element of L holds (v1 "\/" v0) "/\" (v2 "/\" (v0 "/\" v1)) = v2 "/\" (v0 "/\" v1)

proof

let v2, v1, v0 be Element of L; :: thesis:
v0 "\/" v1 = v1 "\/" v0 by A8;
hence (v1 "\/" v0) "/\" (v2 "/\" (v0 "/\" v1)) = v2 "/\" (v0 "/\" v1) by A481; :: thesis:

end;

A721: for v102, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v102 "/\" (v0 "/\" v1)) = (v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" ((v0 "\/" v1) "/\" v102))

proof

let v102, v1, v0 be Element of L; :: thesis:
(v0 "\/" v1) "/\" (v102 "/\" (v0 "/\" v1)) = v102 "/\" (v0 "/\" v1) by A481;
hence (v0 "/\" v1) "\/" (v102 "/\" (v0 "/\" v1)) = (v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" ((v0 "\/" v1) "/\" v102)) by A441; :: thesis:

end;

A724: for v2, v1, v0 being Element of L holds (v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" v2) = (v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" ((v0 "\/" v1) "/\" v2))

proof

end;

A726: for v2, v1, v0 being Element of L holds v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2)) = (v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" ((v0 "\/" v1) "/\" v2))

proof

end;

A728: for v2, v1, v0 being Element of L holds v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2)) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" ((v0 "\/" v1) "/\" v2)))

proof

let v2, v1, v0 be Element of L; :: thesis:
(v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" ((v0 "\/" v1) "/\" v2)) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" ((v0 "\/" v1) "/\" v2))) by A3;
hence v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2)) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" ((v0 "\/" v1) "/\" v2))) by A726; :: thesis:

end;

A732: for v2, v100, v1, v0 being Element of L holds v100 "/\" ((v100 "\/" (v0 "/\" v1)) "/\" (v2 "\/" (v0 "\/" v1))) = v100 "/\" ((v0 "/\" v1) "\/" (v2 "\/" (v0 "\/" v1)))

proof

let v2, v100, v1, v0 be Element of L; :: thesis:
(v0 "/\" v1) "\/" (v2 "\/" (v0 "\/" v1)) = v2 "\/" (v0 "\/" v1) by A497;
hence v100 "/\" ((v100 "\/" (v0 "/\" v1)) "/\" (v2 "\/" (v0 "\/" v1))) = v100 "/\" ((v0 "/\" v1) "\/" (v2 "\/" (v0 "\/" v1))) by A351; :: thesis:

end;

A735: for v3, v0, v2, v1 being Element of L holds v0 "/\" ((v0 "\/" (v1 "/\" v2)) "/\" (v3 "\/" (v1 "\/" v2))) = v0 "/\" (v3 "\/" (v1 "\/" v2))

proof

let v3, v0, v2, v1 be Element of L; :: thesis:
(v1 "/\" v2) "\/" (v3 "\/" (v1 "\/" v2)) = v3 "\/" (v1 "\/" v2) by A497;
hence v0 "/\" ((v0 "\/" (v1 "/\" v2)) "/\" (v3 "\/" (v1 "\/" v2))) = v0 "/\" (v3 "\/" (v1 "\/" v2)) by A732; :: thesis:

end;

A738: for v102, v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" v102 = (v0 "\/" (v1 "/\" v2)) "/\" ((v1 "\/" v0) "/\" v102)

proof

let v102, v0, v2, v1 be Element of L; :: thesis:
(v0 "\/" (v1 "/\" v2)) "/\" (v1 "\/" v0) = v0 "\/" (v1 "/\" v2) by A500;
hence (v0 "\/" (v1 "/\" v2)) "/\" v102 = (v0 "\/" (v1 "/\" v2)) "/\" ((v1 "\/" v0) "/\" v102) by A3; :: thesis:

end;

A743: for v102, v1, v2, v100 being Element of L holds ((v1 "\/" (v100 "/\" (v100 "\/" v2))) "/\" v102) "\/" (v102 "/\" v100) = v102 "/\" (v100 "\/" (v1 "\/" (v100 "/\" v2)))

proof

let v102, v1, v2, v100 be Element of L; :: thesis:
v100 "\/" (v1 "\/" (v100 "/\" v2)) = v1 "\/" (v100 "/\" (v100 "\/" v2)) by A421;
hence ((v1 "\/" (v100 "/\" (v100 "\/" v2))) "/\" v102) "\/" (v102 "/\" v100) = v102 "/\" (v100 "\/" (v1 "\/" (v100 "/\" v2))) by A513; :: thesis:

end;

A747: for v101, v1, v102 being Element of L holds (v102 "\/" v1) "\/" (v101 "/\" (v102 "\/" v1)) = (v102 "\/" v1) "\/" (v101 "/\" v102)

proof

let v101, v1, v102 be Element of L; :: thesis:
((v102 "\/" v1) "/\" v101) "\/" (v101 "/\" v102) = v101 "/\" (v102 "\/" v1) by A513;
hence (v102 "\/" v1) "\/" (v101 "/\" (v102 "\/" v1)) = (v102 "\/" v1) "\/" (v101 "/\" v102) by A426; :: thesis:

end;

A750: for v2, v1, v0 being Element of L holds (v0 "\/" v1) "/\" ((v0 "\/" v1) "\/" v2) = (v0 "\/" v1) "\/" (v2 "/\" v0)

proof

let v2, v1, v0 be Element of L; :: thesis:
(v0 "\/" v1) "\/" (v2 "/\" (v0 "\/" v1)) = (v0 "\/" v1) "/\" ((v0 "\/" v1) "\/" v2) by A400;
hence (v0 "\/" v1) "/\" ((v0 "\/" v1) "\/" v2) = (v0 "\/" v1) "\/" (v2 "/\" v0) by A747; :: thesis:

end;

A752: for v0, v2, v1 being Element of L holds (v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" v2)) = (v0 "\/" v1) "\/" (v2 "/\" v0)

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) by A7;
hence (v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" v2)) = (v0 "\/" v1) "\/" (v2 "/\" v0) by A750; :: thesis:

end;

A754: for v0, v2, v1 being Element of L holds (v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" v2)) = v0 "\/" (v1 "\/" (v2 "/\" v0))

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "\/" v1) "\/" (v2 "/\" v0) = v0 "\/" (v1 "\/" (v2 "/\" v0)) by A7;
hence (v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" v2)) = v0 "\/" (v1 "\/" (v2 "/\" v0)) by A752; :: thesis:

end;

A758: for v102, v1, v100 being Element of L holds v100 "\/" (v102 "/\" (v100 "\/" v1)) = ((v100 "\/" v1) "/\" v102) "\/" (v100 "/\" (v100 "\/" v102))

proof

let v102, v1, v100 be Element of L; :: thesis:
((v100 "\/" v1) "/\" v102) "\/" (v102 "/\" v100) = v102 "/\" (v100 "\/" v1) by A513;
hence v100 "\/" (v102 "/\" (v100 "\/" v1)) = ((v100 "\/" v1) "/\" v102) "\/" (v100 "/\" (v100 "\/" v102)) by A451; :: thesis:

end;

A764: for v102, v1, v2, v100 being Element of L holds ((v1 "\/" (v100 "/\" (v100 "\/" v2))) "/\" v102) "\/" (v102 "/\" v100) = v102 "/\" (v100 "\/" (v1 "\/" (v2 "/\" v100)))

proof

let v102, v1, v2, v100 be Element of L; :: thesis:
v100 "\/" (v1 "\/" (v2 "/\" v100)) = v1 "\/" (v100 "/\" (v100 "\/" v2)) by A451;
hence ((v1 "\/" (v100 "/\" (v100 "\/" v2))) "/\" v102) "\/" (v102 "/\" v100) = v102 "/\" (v100 "\/" (v1 "\/" (v2 "/\" v100))) by A513; :: thesis:

end;

A767: for v3, v0, v2, v1 being Element of L holds v3 "/\" (v1 "\/" (v0 "\/" (v1 "/\" v2))) = v3 "/\" (v1 "\/" (v0 "\/" (v2 "/\" v1)))

proof

let v3, v0, v2, v1 be Element of L; :: thesis:
((v0 "\/" (v1 "/\" (v1 "\/" v2))) "/\" v3) "\/" (v3 "/\" v1) = v3 "/\" (v1 "\/" (v0 "\/" (v1 "/\" v2))) by A743;
hence v3 "/\" (v1 "\/" (v0 "\/" (v1 "/\" v2))) = v3 "/\" (v1 "\/" (v0 "\/" (v2 "/\" v1))) by A764; :: thesis:

end;

A770: for v0, v2, v3, v1 being Element of L holds v0 "/\" (v1 "\/" (v2 "\/" (v1 "/\" v3))) = v0 "/\" ((v1 "\/" v2) "/\" (v1 "\/" (v2 "\/" v3)))

proof

let v0, v2, v3, v1 be Element of L; :: thesis:
v1 "\/" (v2 "\/" (v3 "/\" v1)) = (v1 "\/" v2) "/\" (v1 "\/" (v2 "\/" v3)) by A754;
hence v0 "/\" (v1 "\/" (v2 "\/" (v1 "/\" v3))) = v0 "/\" ((v1 "\/" v2) "/\" (v1 "\/" (v2 "\/" v3))) by A767; :: thesis:

end;

A772: for v1, v2, v3, v0 being Element of L holds (v0 "/\" v1) "\/" (v1 "/\" (v2 "\/" (v0 "/\" (v0 "\/" v3)))) = v1 "/\" ((v0 "\/" v2) "/\" (v0 "\/" (v2 "\/" v3)))

proof

let v1, v2, v3, v0 be Element of L; :: thesis:
v1 "/\" (v0 "\/" (v2 "\/" (v0 "/\" v3))) = v1 "/\" ((v0 "\/" v2) "/\" (v0 "\/" (v2 "\/" v3))) by A770;
hence (v0 "/\" v1) "\/" (v1 "/\" (v2 "\/" (v0 "/\" (v0 "\/" v3)))) = v1 "/\" ((v0 "\/" v2) "/\" (v0 "\/" (v2 "\/" v3))) by A675; :: thesis:

end;

A774: for v0, v2, v1 being Element of L holds (v0 "\/" v1) "/\" ((v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" v2))) = v0 "\/" (v1 "\/" (v0 "/\" v2))

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" (v0 "/\" v2))) = (v0 "\/" v1) "/\" ((v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" v2))) by A770;
hence (v0 "\/" v1) "/\" ((v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" v2))) = v0 "\/" (v1 "\/" (v0 "/\" v2)) by A510; :: thesis:

end;

A776: for v0, v2, v1 being Element of L holds (v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" v2)) = v0 "\/" (v1 "\/" (v0 "/\" v2))

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "\/" v1) "/\" ((v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" v2))) = (v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" v2)) by A26;
hence (v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" v2)) = v0 "\/" (v1 "\/" (v0 "/\" v2)) by A774; :: thesis:

end;

A779: for v2, v1, v0 being Element of L holds (v0 "\/" (v0 "/\" v1)) "/\" (v0 "\/" ((v0 "/\" v1) "\/" ((v0 "\/" v1) "/\" v2))) = v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" ((v0 "/\" v1) "\/" v2)))

proof

let v2, v1, v0 be Element of L; :: thesis:
v0 "\/" ((v0 "/\" v1) "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) = (v0 "\/" (v0 "/\" v1)) "/\" (v0 "\/" ((v0 "/\" v1) "\/" ((v0 "\/" v1) "/\" v2))) by A776;
hence (v0 "\/" (v0 "/\" v1)) "/\" (v0 "\/" ((v0 "/\" v1) "\/" ((v0 "\/" v1) "/\" v2))) = v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" ((v0 "/\" v1) "\/" v2))) by A614; :: thesis:

end;

A781: for v2, v1, v0 being Element of L holds (v0 "/\" (v0 "\/" v1)) "/\" (v0 "\/" ((v0 "/\" v1) "\/" ((v0 "\/" v1) "/\" v2))) = v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" ((v0 "/\" v1) "\/" v2)))

proof

let v2, v1, v0 be Element of L; :: thesis:
v0 "\/" (v0 "/\" v1) = v0 "/\" (v0 "\/" v1) by A347;
hence (v0 "/\" (v0 "\/" v1)) "/\" (v0 "\/" ((v0 "/\" v1) "\/" ((v0 "\/" v1) "/\" v2))) = v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" ((v0 "/\" v1) "\/" v2))) by A779; :: thesis:

end;

A783: for v2, v1, v0 being Element of L holds (v0 "/\" (v0 "\/" v1)) "/\" (v0 "\/" ((v0 "\/" v1) "/\" v2)) = v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" ((v0 "/\" v1) "\/" v2)))

proof

let v2, v1, v0 be Element of L; :: thesis:
v0 "\/" ((v0 "/\" v1) "\/" ((v0 "\/" v1) "/\" v2)) = v0 "\/" ((v0 "\/" v1) "/\" v2) by A696;
hence (v0 "/\" (v0 "\/" v1)) "/\" (v0 "\/" ((v0 "\/" v1) "/\" v2)) = v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" ((v0 "/\" v1) "\/" v2))) by A781; :: thesis:

end;

A785: for v2, v1, v0 being Element of L holds v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" ((v0 "\/" v1) "/\" v2))) = v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" ((v0 "/\" v1) "\/" v2)))

proof

let v2, v1, v0 be Element of L; :: thesis:
(v0 "/\" (v0 "\/" v1)) "/\" (v0 "\/" ((v0 "\/" v1) "/\" v2)) = v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" ((v0 "\/" v1) "/\" v2))) by A3;
hence v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" ((v0 "\/" v1) "/\" v2))) = v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" ((v0 "/\" v1) "\/" v2))) by A783; :: thesis:

end;

A787: for v2, v1, v0 being Element of L holds v0 "/\" (v0 "\/" ((v0 "\/" v1) "/\" v2)) = v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" ((v0 "/\" v1) "\/" v2)))

proof

let v2, v1, v0 be Element of L; :: thesis:
(v0 "\/" v1) "/\" (v0 "\/" ((v0 "\/" v1) "/\" v2)) = v0 "\/" ((v0 "\/" v1) "/\" v2) by A198;
hence v0 "/\" (v0 "\/" ((v0 "\/" v1) "/\" v2)) = v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" ((v0 "/\" v1) "\/" v2))) by A785; :: thesis:

end;

A790: for v2, v1, v0 being Element of L holds v0 "\/" ((v0 "/\" v1) "\/" (v2 "/\" (v0 "/\" (v0 "\/" v1)))) = v0 "/\" (v0 "\/" ((v0 "\/" v1) "/\" v2))

proof

let v2, v1, v0 be Element of L; :: thesis:
v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" ((v0 "/\" v1) "\/" v2))) = v0 "/\" (v0 "\/" ((v0 "\/" v1) "/\" v2)) by A787;
hence v0 "\/" ((v0 "/\" v1) "\/" (v2 "/\" (v0 "/\" (v0 "\/" v1)))) = v0 "/\" (v0 "\/" ((v0 "\/" v1) "/\" v2)) by A622; :: thesis:

end;

A793: for v102, v100, v1 being Element of L holds (v1 "/\" v100) "\/" ((v102 "\/" (v1 "/\" (v1 "\/" v100))) "/\" v100) = v100 "/\" ((v1 "/\" (v1 "\/" v100)) "\/" v102)

proof

let v102, v100, v1 be Element of L; :: thesis:
v100 "/\" (v1 "/\" (v1 "\/" v100)) = v1 "/\" v100 by A308;
hence (v1 "/\" v100) "\/" ((v102 "\/" (v1 "/\" (v1 "\/" v100))) "/\" v100) = v100 "/\" ((v1 "/\" (v1 "\/" v100)) "\/" v102) by A517; :: thesis:

end;

A796: for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v1 "/\" (v2 "\/" (v0 "/\" (v0 "\/" v1)))) = v1 "/\" ((v0 "/\" (v0 "\/" v1)) "\/" v2)

proof

let v2, v1, v0 be Element of L; :: thesis:
(v2 "\/" (v0 "/\" (v0 "\/" v1))) "/\" v1 = v1 "/\" (v2 "\/" (v0 "/\" (v0 "\/" v1))) by A4;
hence (v0 "/\" v1) "\/" (v1 "/\" (v2 "\/" (v0 "/\" (v0 "\/" v1)))) = v1 "/\" ((v0 "/\" (v0 "\/" v1)) "\/" v2) by A793; :: thesis:

end;

A798: for v0, v1, v2 being Element of L holds v1 "/\" ((v0 "\/" v2) "/\" (v0 "\/" (v2 "\/" v1))) = v1 "/\" ((v0 "/\" (v0 "\/" v1)) "\/" v2)

proof

let v0, v1, v2 be Element of L; :: thesis:
(v0 "/\" v1) "\/" (v1 "/\" (v2 "\/" (v0 "/\" (v0 "\/" v1)))) = v1 "/\" ((v0 "\/" v2) "/\" (v0 "\/" (v2 "\/" v1))) by A772;
hence v1 "/\" ((v0 "\/" v2) "/\" (v0 "\/" (v2 "\/" v1))) = v1 "/\" ((v0 "/\" (v0 "\/" v1)) "\/" v2) by A796; :: thesis:

end;

A801: for v0, v2, v1 being Element of L holds (v1 "\/" v2) "/\" v0 = v0 "/\" ((v1 "/\" (v1 "\/" v0)) "\/" v2)

proof

let v0, v2, v1 be Element of L; :: thesis:
v0 "/\" ((v1 "\/" v2) "/\" (v1 "\/" (v2 "\/" v0))) = (v1 "\/" v2) "/\" v0 by A328;
hence (v1 "\/" v2) "/\" v0 = v0 "/\" ((v1 "/\" (v1 "\/" v0)) "\/" v2) by A798; :: thesis:

end;

A804: for v2, v1, v0 being Element of L holds (v0 "\/" v1) "/\" v2 = v2 "/\" (v0 "\/" ((v0 "/\" v2) "\/" v1))

proof

let v2, v1, v0 be Element of L; :: thesis:
(v0 "/\" (v0 "\/" v2)) "\/" v1 = v0 "\/" ((v0 "/\" v2) "\/" v1) by A403;
hence (v0 "\/" v1) "/\" v2 = v2 "/\" (v0 "\/" ((v0 "/\" v2) "\/" v1)) by A801; :: thesis:

end;

A808: for v2, v1, v0 being Element of L holds v0 "\/" ((v0 "/\" v1) "\/" ((v0 "\/" v1) "/\" v2)) = (v0 "\/" v1) "/\" (v2 "\/" ((v0 "\/" v2) "/\" (v0 "\/" v1)))

proof

let v2, v1, v0 be Element of L; :: thesis:
v2 "/\" (v0 "\/" ((v0 "/\" v2) "\/" v1)) = (v0 "\/" v1) "/\" v2 by A804;
hence v0 "\/" ((v0 "/\" v1) "\/" ((v0 "\/" v1) "/\" v2)) = (v0 "\/" v1) "/\" (v2 "\/" ((v0 "\/" v2) "/\" (v0 "\/" v1))) by A689; :: thesis:

end;

A810: for v2, v1, v0 being Element of L holds v0 "\/" ((v0 "\/" v1) "/\" v2) = (v0 "\/" v1) "/\" (v2 "\/" ((v0 "\/" v2) "/\" (v0 "\/" v1)))

proof

let v2, v1, v0 be Element of L; :: thesis:
v0 "\/" ((v0 "/\" v1) "\/" ((v0 "\/" v1) "/\" v2)) = v0 "\/" ((v0 "\/" v1) "/\" v2) by A696;
hence v0 "\/" ((v0 "\/" v1) "/\" v2) = (v0 "\/" v1) "/\" (v2 "\/" ((v0 "\/" v2) "/\" (v0 "\/" v1))) by A808; :: thesis:

end;

A813: for v1, v2, v102, v101 being Element of L holds ((v1 "/\" ((v101 "/\" v102) "/\" v2)) "/\" v101) "\/" ((v101 "/\" v102) "/\" ((v101 "/\" v102) "\/" (v1 "/\" v2))) = (v1 "/\" ((v101 "/\" v102) "/\" v2)) "\/" (v101 "/\" v102)

proof

let v1, v2, v102, v101 be Element of L; :: thesis:
(v101 "/\" v102) "\/" (v1 "/\" ((v101 "/\" v102) "/\" v2)) = (v101 "/\" v102) "/\" ((v101 "/\" v102) "\/" (v1 "/\" v2)) by A417;
hence ((v1 "/\" ((v101 "/\" v102) "/\" v2)) "/\" v101) "\/" ((v101 "/\" v102) "/\" ((v101 "/\" v102) "\/" (v1 "/\" v2))) = (v1 "/\" ((v101 "/\" v102) "/\" v2)) "\/" (v101 "/\" v102) by A529; :: thesis:

end;

A816: for v0, v1, v3, v2 being Element of L holds ((v0 "/\" (v1 "/\" (v2 "/\" v3))) "/\" v1) "\/" ((v1 "/\" v2) "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3))) = (v0 "/\" ((v1 "/\" v2) "/\" v3)) "\/" (v1 "/\" v2)

proof

let v0, v1, v3, v2 be Element of L; :: thesis:
(v1 "/\" v2) "/\" v3 = v1 "/\" (v2 "/\" v3) by A3;
hence ((v0 "/\" (v1 "/\" (v2 "/\" v3))) "/\" v1) "\/" ((v1 "/\" v2) "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3))) = (v0 "/\" ((v1 "/\" v2) "/\" v3)) "\/" (v1 "/\" v2) by A813; :: thesis:

end;

A818: for v0, v1, v3, v2 being Element of L holds (v1 "/\" (v0 "/\" (v1 "/\" (v2 "/\" v3)))) "\/" ((v1 "/\" v2) "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3))) = (v0 "/\" ((v1 "/\" v2) "/\" v3)) "\/" (v1 "/\" v2)

proof

let v0, v1, v3, v2 be Element of L; :: thesis:
(v0 "/\" (v1 "/\" (v2 "/\" v3))) "/\" v1 = v1 "/\" (v0 "/\" (v1 "/\" (v2 "/\" v3))) by A4;
hence (v1 "/\" (v0 "/\" (v1 "/\" (v2 "/\" v3)))) "\/" ((v1 "/\" v2) "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3))) = (v0 "/\" ((v1 "/\" v2) "/\" v3)) "\/" (v1 "/\" v2) by A816; :: thesis:

end;

A821: for v1, v0, v3, v2 being Element of L holds (v1 "/\" (v0 "/\" (v2 "/\" v3))) "\/" ((v0 "/\" v2) "/\" ((v0 "/\" v2) "\/" (v1 "/\" v3))) = (v1 "/\" ((v0 "/\" v2) "/\" v3)) "\/" (v0 "/\" v2)

proof

let v1, v0, v3, v2 be Element of L; :: thesis:
v0 "/\" (v1 "/\" (v0 "/\" (v2 "/\" v3))) = v1 "/\" (v0 "/\" (v2 "/\" v3)) by A162;
hence (v1 "/\" (v0 "/\" (v2 "/\" v3))) "\/" ((v0 "/\" v2) "/\" ((v0 "/\" v2) "\/" (v1 "/\" v3))) = (v1 "/\" ((v0 "/\" v2) "/\" v3)) "\/" (v0 "/\" v2) by A818; :: thesis:

end;

A824: for v0, v1, v3, v2 being Element of L holds (v0 "/\" (v1 "/\" (v2 "/\" v3))) "\/" (v1 "/\" (v2 "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3)))) = (v0 "/\" ((v1 "/\" v2) "/\" v3)) "\/" (v1 "/\" v2)

proof

let v0, v1, v3, v2 be Element of L; :: thesis:
(v1 "/\" v2) "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3)) = v1 "/\" (v2 "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3))) by A3;
hence (v0 "/\" (v1 "/\" (v2 "/\" v3))) "\/" (v1 "/\" (v2 "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3)))) = (v0 "/\" ((v1 "/\" v2) "/\" v3)) "\/" (v1 "/\" v2) by A821; :: thesis:

end;

A826: for v2, v0, v3, v1 being Element of L holds v1 "/\" (v2 "/\" ((v2 "\/" (v0 "/\" (v1 "/\" v3))) "/\" (v1 "\/" (v0 "/\" (v2 "/\" v3))))) = (v0 "/\" ((v1 "/\" v2) "/\" v3)) "\/" (v1 "/\" v2)

proof

let v2, v0, v3, v1 be Element of L; :: thesis:
(v0 "/\" (v1 "/\" (v2 "/\" v3))) "\/" (v1 "/\" (v2 "/\" ((v1 "/\" v2) "\/" (v0 "/\" v3)))) = v1 "/\" (v2 "/\" ((v2 "\/" (v0 "/\" (v1 "/\" v3))) "/\" (v1 "\/" (v0 "/\" (v2 "/\" v3))))) by A666;
hence v1 "/\" (v2 "/\" ((v2 "\/" (v0 "/\" (v1 "/\" v3))) "/\" (v1 "\/" (v0 "/\" (v2 "/\" v3))))) = (v0 "/\" ((v1 "/\" v2) "/\" v3)) "\/" (v1 "/\" v2) by A824; :: thesis:

end;

A829: for v1, v2, v3, v0 being Element of L holds v0 "/\" (v1 "/\" ((v1 "\/" (v2 "/\" (v0 "/\" v3))) "/\" (v0 "\/" (v2 "/\" (v1 "/\" v3))))) = (v2 "/\" (v0 "/\" (v1 "/\" v3))) "\/" (v0 "/\" v1)

proof

let v1, v2, v3, v0 be Element of L; :: thesis:
(v0 "/\" v1) "/\" v3 = v0 "/\" (v1 "/\" v3) by A3;
hence v0 "/\" (v1 "/\" ((v1 "\/" (v2 "/\" (v0 "/\" v3))) "/\" (v0 "\/" (v2 "/\" (v1 "/\" v3))))) = (v2 "/\" (v0 "/\" (v1 "/\" v3))) "\/" (v0 "/\" v1) by A826; :: thesis:

end;

A831: for v1, v2, v3, v0 being Element of L holds v0 "/\" (v1 "/\" ((v1 "\/" (v2 "/\" (v0 "/\" v3))) "/\" (v0 "\/" (v2 "/\" (v1 "/\" v3))))) = (v0 "/\" v1) "\/" (v2 "/\" (v0 "/\" (v1 "/\" v3)))

proof

let v1, v2, v3, v0 be Element of L; :: thesis:
(v2 "/\" (v0 "/\" (v1 "/\" v3))) "\/" (v0 "/\" v1) = (v0 "/\" v1) "\/" (v2 "/\" (v0 "/\" (v1 "/\" v3))) by A8;
hence v0 "/\" (v1 "/\" ((v1 "\/" (v2 "/\" (v0 "/\" v3))) "/\" (v0 "\/" (v2 "/\" (v1 "/\" v3))))) = (v0 "/\" v1) "\/" (v2 "/\" (v0 "/\" (v1 "/\" v3))) by A829; :: thesis:

end;

A833: for v1, v2, v3, v0 being Element of L holds v0 "/\" (v1 "/\" ((v1 "\/" (v2 "/\" (v0 "/\" v3))) "/\" (v0 "\/" (v2 "/\" (v1 "/\" v3))))) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" (v2 "/\" v3)))

proof

let v1, v2, v3, v0 be Element of L; :: thesis:
(v0 "/\" v1) "\/" (v2 "/\" (v0 "/\" (v1 "/\" v3))) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" (v2 "/\" v3))) by A628;
hence v0 "/\" (v1 "/\" ((v1 "\/" (v2 "/\" (v0 "/\" v3))) "/\" (v0 "\/" (v2 "/\" (v1 "/\" v3))))) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" (v2 "/\" v3))) by A831; :: thesis:

end;

A836: for v2, v1, v0 being Element of L holds v0 "/\" (v1 "/\" ((v1 "\/" ((v0 "\/" v1) "/\" (v0 "/\" v2))) "/\" (v0 "\/" ((v0 "\/" v1) "/\" (v1 "/\" v2))))) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2))

proof

let v2, v1, v0 be Element of L; :: thesis:
v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" ((v0 "\/" v1) "/\" v2))) = v0 "/\" (v1 "/\" ((v1 "\/" ((v0 "\/" v1) "/\" (v0 "/\" v2))) "/\" (v0 "\/" ((v0 "\/" v1) "/\" (v1 "/\" v2))))) by A833;
hence v0 "/\" (v1 "/\" ((v1 "\/" ((v0 "\/" v1) "/\" (v0 "/\" v2))) "/\" (v0 "\/" ((v0 "\/" v1) "/\" (v1 "/\" v2))))) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2)) by A728; :: thesis:

end;

A838: for v2, v1, v0 being Element of L holds v0 "/\" (v1 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "\/" ((v0 "\/" v1) "/\" (v1 "/\" v2))))) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2))

proof

let v2, v1, v0 be Element of L; :: thesis:
(v0 "\/" v1) "/\" (v0 "/\" v2) = v0 "/\" ((v0 "\/" v1) "/\" v2) by A40;
hence v0 "/\" (v1 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "\/" ((v0 "\/" v1) "/\" (v1 "/\" v2))))) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2)) by A836; :: thesis:

end;

A840: for v2, v1, v0 being Element of L holds v0 "/\" (v1 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "\/" (v1 "/\" ((v0 "\/" v1) "/\" v2))))) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2))

proof

let v2, v1, v0 be Element of L; :: thesis:
(v0 "\/" v1) "/\" (v1 "/\" v2) = v1 "/\" ((v0 "\/" v1) "/\" v2) by A40;
hence v0 "/\" (v1 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "\/" (v1 "/\" ((v0 "\/" v1) "/\" v2))))) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2)) by A838; :: thesis:

end;

A843: for v2, v1, v0 being Element of L holds v0 "/\" (v1 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" (v0 "/\" v2)))) "/\" (v0 "\/" (v1 "/\" ((v0 "\/" v1) "/\" (v0 "/\" v2)))))) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2))

proof

let v2, v1, v0 be Element of L; :: thesis:
v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" (v0 "/\" v2))) = v0 "/\" (v1 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" (v0 "/\" v2)))) "/\" (v0 "\/" (v1 "/\" ((v0 "\/" v1) "/\" (v0 "/\" v2)))))) by A840;
hence v0 "/\" (v1 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" (v0 "/\" v2)))) "/\" (v0 "\/" (v1 "/\" ((v0 "\/" v1) "/\" (v0 "/\" v2)))))) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2)) by A714; :: thesis:

end;

A845: for v2, v1, v0 being Element of L holds v0 "/\" (v1 "/\" ((v1 "\/" (v0 "/\" (v0 "/\" ((v0 "\/" v1) "/\" v2)))) "/\" (v0 "\/" (v1 "/\" ((v0 "\/" v1) "/\" (v0 "/\" v2)))))) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2))

proof

let v2, v1, v0 be Element of L; :: thesis:
(v0 "\/" v1) "/\" (v0 "/\" v2) = v0 "/\" ((v0 "\/" v1) "/\" v2) by A40;
hence v0 "/\" (v1 "/\" ((v1 "\/" (v0 "/\" (v0 "/\" ((v0 "\/" v1) "/\" v2)))) "/\" (v0 "\/" (v1 "/\" ((v0 "\/" v1) "/\" (v0 "/\" v2)))))) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2)) by A843; :: thesis:

end;

A847: for v2, v1, v0 being Element of L holds v0 "/\" (v1 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "\/" (v1 "/\" ((v0 "\/" v1) "/\" (v0 "/\" v2)))))) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2))

proof

let v2, v1, v0 be Element of L; :: thesis:
v0 "/\" (v0 "/\" ((v0 "\/" v1) "/\" v2)) = v0 "/\" ((v0 "\/" v1) "/\" v2) by A26;
hence v0 "/\" (v1 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "\/" (v1 "/\" ((v0 "\/" v1) "/\" (v0 "/\" v2)))))) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2)) by A845; :: thesis:

end;

A849: for v2, v1, v0 being Element of L holds v0 "/\" (v1 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "\/" (v1 "/\" (v0 "/\" ((v0 "\/" v1) "/\" v2)))))) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2))

proof

let v2, v1, v0 be Element of L; :: thesis:
(v0 "\/" v1) "/\" (v0 "/\" v2) = v0 "/\" ((v0 "\/" v1) "/\" v2) by A40;
hence v0 "/\" (v1 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "\/" (v1 "/\" (v0 "/\" ((v0 "\/" v1) "/\" v2)))))) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2)) by A847; :: thesis:

end;

A851: for v2, v1, v0 being Element of L holds v0 "/\" (v1 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "\/" (v0 "/\" (v1 "/\" v2))))) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2))

proof

let v2, v1, v0 be Element of L; :: thesis:
v1 "/\" (v0 "/\" ((v0 "\/" v1) "/\" v2)) = v0 "/\" (v1 "/\" v2) by A323;
hence v0 "/\" (v1 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "\/" (v0 "/\" (v1 "/\" v2))))) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2)) by A849; :: thesis:

end;

A853: for v2, v1, v0 being Element of L holds v0 "/\" (v1 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "/\" (v0 "\/" (v1 "/\" v2))))) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2))

proof

let v2, v1, v0 be Element of L; :: thesis:
v0 "\/" (v0 "/\" (v1 "/\" v2)) = v0 "/\" (v0 "\/" (v1 "/\" v2)) by A347;
hence v0 "/\" (v1 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "/\" (v0 "\/" (v1 "/\" v2))))) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2)) by A851; :: thesis:

end;

A855: for v2, v1, v0 being Element of L holds v0 "/\" (v1 "/\" (v0 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "\/" (v1 "/\" v2))))) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2))

proof

let v2, v1, v0 be Element of L; :: thesis:
(v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "/\" (v0 "\/" (v1 "/\" v2))) = v0 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "\/" (v1 "/\" v2))) by A40;
hence v0 "/\" (v1 "/\" (v0 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "\/" (v1 "/\" v2))))) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2)) by A853; :: thesis:

end;

A857: for v2, v1, v0 being Element of L holds v1 "/\" (v0 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "\/" (v1 "/\" v2)))) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2))

proof

let v2, v1, v0 be Element of L; :: thesis:
v0 "/\" (v1 "/\" (v0 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "\/" (v1 "/\" v2))))) = v1 "/\" (v0 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "\/" (v1 "/\" v2)))) by A162;
hence v1 "/\" (v0 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "\/" (v1 "/\" v2)))) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2)) by A855; :: thesis:

end;

A860: for v2, v0, v1 being Element of L holds v0 "/\" (v1 "/\" ((v0 "\/" (v1 "/\" ((v1 "\/" v0) "/\" v2))) "/\" (v1 "\/" (v0 "/\" v2)))) = v1 "/\" (v0 "/\" ((v0 "\/" (v1 "/\" ((v1 "\/" v0) "/\" v2))) "/\" (v1 "\/" (v0 "/\" ((v1 "\/" v0) "/\" v2)))))

proof

let v2, v0, v1 be Element of L; :: thesis:
v1 "/\" (v0 "/\" ((v1 "/\" v0) "\/" v2)) = v1 "/\" (v0 "/\" ((v0 "\/" (v1 "/\" ((v1 "\/" v0) "/\" v2))) "/\" (v1 "\/" (v0 "/\" ((v1 "\/" v0) "/\" v2))))) by A840;
hence v0 "/\" (v1 "/\" ((v0 "\/" (v1 "/\" ((v1 "\/" v0) "/\" v2))) "/\" (v1 "\/" (v0 "/\" v2)))) = v1 "/\" (v0 "/\" ((v0 "\/" (v1 "/\" ((v1 "\/" v0) "/\" v2))) "/\" (v1 "\/" (v0 "/\" ((v1 "\/" v0) "/\" v2))))) by A857; :: thesis:

end;

A864: for v2, v1, v0 being Element of L holds v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2)) = v1 "/\" (v0 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "\/" (v1 "/\" v2))))

proof

let v2, v1, v0 be Element of L; :: thesis:
v0 "/\" (v1 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "\/" (v1 "/\" ((v0 "\/" v1) "/\" v2))))) = v1 "/\" (v0 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "\/" (v1 "/\" v2)))) by A860;
hence v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2)) = v1 "/\" (v0 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "\/" (v1 "/\" v2)))) by A840; :: thesis:

end;

A867: for v102, v1, v100 being Element of L holds v100 "\/" ((v100 "/\" v1) "\/" (v102 "/\" (v100 "/\" v1))) = v100 "\/" (v102 "/\" (v100 "/\" v1))

proof

let v102, v1, v100 be Element of L; :: thesis:
v100 "/\" (v100 "/\" v1) = v100 "/\" v1 by A26;
hence v100 "\/" ((v100 "/\" v1) "\/" (v102 "/\" (v100 "/\" v1))) = v100 "\/" (v102 "/\" (v100 "/\" v1)) by A558; :: thesis:

end;

A870: for v2, v1, v0 being Element of L holds v0 "\/" ((v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" v2)) = v0 "\/" (v2 "/\" (v0 "/\" v1))

proof

let v2, v1, v0 be Element of L; :: thesis:
(v0 "/\" v1) "\/" (v2 "/\" (v0 "/\" v1)) = (v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" v2) by A400;
hence v0 "\/" ((v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" v2)) = v0 "\/" (v2 "/\" (v0 "/\" v1)) by A867; :: thesis:

end;

A872: for v2, v1, v0 being Element of L holds v0 "\/" (v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2))) = v0 "\/" (v2 "/\" (v0 "/\" v1))

proof

let v2, v1, v0 be Element of L; :: thesis:
(v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" v2) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2)) by A3;
hence v0 "\/" (v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2))) = v0 "\/" (v2 "/\" (v0 "/\" v1)) by A870; :: thesis:

end;

A874: for v2, v1, v0 being Element of L holds v0 "\/" (v1 "/\" (v0 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "\/" (v1 "/\" v2))))) = v0 "\/" (v2 "/\" (v0 "/\" v1))

proof

let v2, v1, v0 be Element of L; :: thesis:
v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2)) = v1 "/\" (v0 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "\/" (v1 "/\" v2)))) by A864;
hence v0 "\/" (v1 "/\" (v0 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "\/" (v1 "/\" v2))))) = v0 "\/" (v2 "/\" (v0 "/\" v1)) by A872; :: thesis:

end;

A876: for v2, v1, v0 being Element of L holds v0 "/\" (v0 "\/" (v1 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "\/" (v1 "/\" v2))))) = v0 "\/" (v2 "/\" (v0 "/\" v1))

proof

let v2, v1, v0 be Element of L; :: thesis:
v0 "\/" (v1 "/\" (v0 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "\/" (v1 "/\" v2))))) = v0 "/\" (v0 "\/" (v1 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "\/" (v1 "/\" v2))))) by A417;
hence v0 "/\" (v0 "\/" (v1 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "\/" (v1 "/\" v2))))) = v0 "\/" (v2 "/\" (v0 "/\" v1)) by A874; :: thesis:

end;

A878: for v2, v1, v0 being Element of L holds v0 "/\" (v0 "\/" (v1 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "\/" (v1 "/\" v2))))) = v0 "/\" (v0 "\/" (v2 "/\" v1))

proof

let v2, v1, v0 be Element of L; :: thesis:
v0 "\/" (v2 "/\" (v0 "/\" v1)) = v0 "/\" (v0 "\/" (v2 "/\" v1)) by A417;
hence v0 "/\" (v0 "\/" (v1 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "\/" (v1 "/\" v2))))) = v0 "/\" (v0 "\/" (v2 "/\" v1)) by A876; :: thesis:

end;

A881: for v102, v1, v100 being Element of L holds v100 "\/" (v100 "\/" ((v100 "/\" v1) "\/" (v102 "/\" (v100 "\/" v1)))) = v100 "\/" (v102 "/\" (v100 "\/" v1))

proof

let v102, v1, v100 be Element of L; :: thesis:
(v100 "/\" (v100 "\/" v1)) "\/" (v102 "/\" (v100 "\/" v1)) = v100 "\/" ((v100 "/\" v1) "\/" (v102 "/\" (v100 "\/" v1))) by A403;
hence v100 "\/" (v100 "\/" ((v100 "/\" v1) "\/" (v102 "/\" (v100 "\/" v1)))) = v100 "\/" (v102 "/\" (v100 "\/" v1)) by A558; :: thesis:

end;

A884: for v2, v1, v0 being Element of L holds v0 "\/" ((v0 "/\" v1) "\/" (v2 "/\" (v0 "\/" v1))) = v0 "\/" (v2 "/\" (v0 "\/" v1))

proof

let v2, v1, v0 be Element of L; :: thesis:
v0 "\/" (v0 "\/" ((v0 "/\" v1) "\/" (v2 "/\" (v0 "\/" v1)))) = v0 "\/" ((v0 "/\" v1) "\/" (v2 "/\" (v0 "\/" v1))) by A43;
hence v0 "\/" ((v0 "/\" v1) "\/" (v2 "/\" (v0 "\/" v1))) = v0 "\/" (v2 "/\" (v0 "\/" v1)) by A881; :: thesis:

end;

A887: for v101, v2, v1 being Element of L holds (v1 "\/" (v101 "/\" (v1 "\/" v2))) "\/" (v101 "/\" (v1 "\/" v2)) = (v1 "\/" (v101 "/\" (v1 "\/" v2))) "/\" ((v1 "\/" (v101 "/\" (v1 "\/" v2))) "\/" v101)

proof

let v101, v2, v1 be Element of L; :: thesis:
v101 "/\" (v1 "\/" (v101 "/\" (v1 "\/" v2))) = v101 "/\" (v1 "\/" v2) by A568;
hence (v1 "\/" (v101 "/\" (v1 "\/" v2))) "\/" (v101 "/\" (v1 "\/" v2)) = (v1 "\/" (v101 "/\" (v1 "\/" v2))) "/\" ((v1 "\/" (v101 "/\" (v1 "\/" v2))) "\/" v101) by A400; :: thesis:

end;

A890: for v1, v2, v0 being Element of L holds (v1 "/\" (v0 "\/" v2)) "\/" (v0 "\/" (v1 "/\" (v0 "\/" v2))) = (v0 "\/" (v1 "/\" (v0 "\/" v2))) "/\" ((v0 "\/" (v1 "/\" (v0 "\/" v2))) "\/" v1)

proof

let v1, v2, v0 be Element of L; :: thesis:
(v0 "\/" (v1 "/\" (v0 "\/" v2))) "\/" (v1 "/\" (v0 "\/" v2)) = (v1 "/\" (v0 "\/" v2)) "\/" (v0 "\/" (v1 "/\" (v0 "\/" v2))) by A8;
hence (v1 "/\" (v0 "\/" v2)) "\/" (v0 "\/" (v1 "/\" (v0 "\/" v2))) = (v0 "\/" (v1 "/\" (v0 "\/" v2))) "/\" ((v0 "\/" (v1 "/\" (v0 "\/" v2))) "\/" v1) by A887; :: thesis:

end;

A893: for v0, v2, v1 being Element of L holds v1 "\/" (v0 "/\" (v1 "\/" v2)) = (v1 "\/" (v0 "/\" (v1 "\/" v2))) "/\" ((v1 "\/" (v0 "/\" (v1 "\/" v2))) "\/" v0)

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "/\" (v1 "\/" v2)) "\/" (v1 "\/" (v0 "/\" (v1 "\/" v2))) = v1 "\/" (v0 "/\" (v1 "\/" v2)) by A51;
hence v1 "\/" (v0 "/\" (v1 "\/" v2)) = (v1 "\/" (v0 "/\" (v1 "\/" v2))) "/\" ((v1 "\/" (v0 "/\" (v1 "\/" v2))) "\/" v0) by A890; :: thesis:

end;

A896: for v1, v2, v0 being Element of L holds v0 "\/" (v1 "/\" (v0 "\/" v2)) = (v0 "\/" (v1 "/\" (v0 "\/" v2))) "/\" (v1 "\/" (v0 "\/" (v1 "/\" (v0 "\/" v2))))

proof

let v1, v2, v0 be Element of L; :: thesis:
(v0 "\/" (v1 "/\" (v0 "\/" v2))) "\/" v1 = v1 "\/" (v0 "\/" (v1 "/\" (v0 "\/" v2))) by A8;
hence v0 "\/" (v1 "/\" (v0 "\/" v2)) = (v0 "\/" (v1 "/\" (v0 "\/" v2))) "/\" (v1 "\/" (v0 "\/" (v1 "/\" (v0 "\/" v2)))) by A893; :: thesis:

end;

A898: for v1, v2, v0 being Element of L holds v0 "\/" (v1 "/\" (v0 "\/" v2)) = (v0 "\/" (v1 "/\" (v0 "\/" v2))) "/\" ((v1 "\/" v0) "/\" (v1 "\/" (v0 "\/" (v0 "\/" v2))))

proof

let v1, v2, v0 be Element of L; :: thesis:
v1 "\/" (v0 "\/" (v1 "/\" (v0 "\/" v2))) = (v1 "\/" v0) "/\" (v1 "\/" (v0 "\/" (v0 "\/" v2))) by A776;
hence v0 "\/" (v1 "/\" (v0 "\/" v2)) = (v0 "\/" (v1 "/\" (v0 "\/" v2))) "/\" ((v1 "\/" v0) "/\" (v1 "\/" (v0 "\/" (v0 "\/" v2)))) by A896; :: thesis:

end;

A900: for v1, v2, v0 being Element of L holds v0 "\/" (v1 "/\" (v0 "\/" v2)) = (v0 "\/" (v1 "/\" (v0 "\/" v2))) "/\" ((v1 "\/" v0) "/\" (v1 "\/" (v0 "\/" v2)))

proof

let v1, v2, v0 be Element of L; :: thesis:
v0 "\/" (v0 "\/" v2) = v0 "\/" v2 by A43;
hence v0 "\/" (v1 "/\" (v0 "\/" v2)) = (v0 "\/" (v1 "/\" (v0 "\/" v2))) "/\" ((v1 "\/" v0) "/\" (v1 "\/" (v0 "\/" v2))) by A898; :: thesis:

end;

A902: for v1, v2, v0 being Element of L holds v0 "\/" (v1 "/\" (v0 "\/" v2)) = (v0 "\/" (v1 "/\" (v0 "\/" v2))) "/\" (v1 "\/" (v0 "\/" v2))

proof

let v1, v2, v0 be Element of L; :: thesis:
(v0 "\/" (v1 "/\" (v0 "\/" v2))) "/\" ((v1 "\/" v0) "/\" (v1 "\/" (v0 "\/" v2))) = (v0 "\/" (v1 "/\" (v0 "\/" v2))) "/\" (v1 "\/" (v0 "\/" v2)) by A738;
hence v0 "\/" (v1 "/\" (v0 "\/" v2)) = (v0 "\/" (v1 "/\" (v0 "\/" v2))) "/\" (v1 "\/" (v0 "\/" v2)) by A900; :: thesis:

end;

A905: for v0, v1, v2 being Element of L holds v0 "/\" (v1 "\/" ((v2 "\/" v1) "/\" v0)) = v0 "/\" (v2 "\/" v1)

proof

let v0, v1, v2 be Element of L; :: thesis:
v0 "/\" (v2 "\/" v1) = (v2 "\/" v1) "/\" v0 by A4;
hence v0 "/\" (v1 "\/" ((v2 "\/" v1) "/\" v0)) = v0 "/\" (v2 "\/" v1) by A570; :: thesis:

end;

A908: for v100, v101, v1, v2 being Element of L holds v100 "/\" (v101 "/\" (v2 "\/" v1)) = v101 "/\" (v100 "/\" (v1 "\/" (v101 "/\" (v2 "\/" v1))))

proof

let v100, v101, v1, v2 be Element of L; :: thesis:
v101 "/\" (v1 "\/" (v101 "/\" (v2 "\/" v1))) = v101 "/\" (v2 "\/" v1) by A570;
hence v100 "/\" (v101 "/\" (v2 "\/" v1)) = v101 "/\" (v100 "/\" (v1 "\/" (v101 "/\" (v2 "\/" v1)))) by A40; :: thesis:

end;

A913: for v2, v1, v0 being Element of L holds v0 "\/" ((v0 "\/" v1) "/\" v2) = (v0 "\/" v1) "/\" (v0 "\/" v2)

proof

let v2, v1, v0 be Element of L; :: thesis:
(v0 "\/" v1) "/\" (v2 "\/" ((v0 "\/" v2) "/\" (v0 "\/" v1))) = (v0 "\/" v1) "/\" (v0 "\/" v2) by A905;
hence v0 "\/" ((v0 "\/" v1) "/\" v2) = (v0 "\/" v1) "/\" (v0 "\/" v2) by A810; :: thesis:

end;

A915: for v0, v2, v1 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" (v0 "/\" (v0 "\/" (v1 "/\" v2)))) = (v0 "\/" v1) "/\" (v0 "/\" ((v0 "/\" v1) "\/" v2))

proof

let v0, v2, v1 be Element of L; :: thesis:
v0 "/\" ((v0 "\/" v1) "/\" (v2 "\/" (v0 "/\" ((v0 "/\" v1) "\/" v2)))) = (v0 "\/" v1) "/\" (v0 "/\" ((v0 "/\" v1) "\/" v2)) by A908;
hence (v0 "/\" v1) "\/" (v2 "/\" (v0 "/\" (v0 "\/" (v1 "/\" v2)))) = (v0 "\/" v1) "/\" (v0 "/\" ((v0 "/\" v1) "\/" v2)) by A357; :: thesis:

end;

A917: for v0, v2, v1 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" (v0 "/\" (v0 "\/" (v1 "/\" v2)))) = v0 "/\" ((v0 "\/" v1) "/\" ((v0 "/\" v1) "\/" v2))

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "\/" v1) "/\" (v0 "/\" ((v0 "/\" v1) "\/" v2)) = v0 "/\" ((v0 "\/" v1) "/\" ((v0 "/\" v1) "\/" v2)) by A40;
hence (v0 "/\" v1) "\/" (v2 "/\" (v0 "/\" (v0 "\/" (v1 "/\" v2)))) = v0 "/\" ((v0 "\/" v1) "/\" ((v0 "/\" v1) "\/" v2)) by A915; :: thesis:

end;

A919: for v0, v2, v1 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" (v0 "/\" (v0 "\/" (v1 "/\" v2)))) = v0 "/\" ((v0 "/\" v1) "\/" v2)

proof

let v0, v2, v1 be Element of L; :: thesis:
v0 "/\" ((v0 "\/" v1) "/\" ((v0 "/\" v1) "\/" v2)) = v0 "/\" ((v0 "/\" v1) "\/" v2) by A594;
hence (v0 "/\" v1) "\/" (v2 "/\" (v0 "/\" (v0 "\/" (v1 "/\" v2)))) = v0 "/\" ((v0 "/\" v1) "\/" v2) by A917; :: thesis:

end;

A921: for v2, v1, v0 being Element of L holds v0 "\/" ((v0 "/\" v1) "\/" (v2 "/\" (v0 "/\" (v0 "\/" v1)))) = v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" v2))

proof

let v2, v1, v0 be Element of L; :: thesis:
v0 "\/" ((v0 "\/" v1) "/\" v2) = (v0 "\/" v1) "/\" (v0 "\/" v2) by A913;
hence v0 "\/" ((v0 "/\" v1) "\/" (v2 "/\" (v0 "/\" (v0 "\/" v1)))) = v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" v2)) by A790; :: thesis:

end;

A923: for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v1 "/\" (v1 "\/" ((v1 "/\" v2) "\/" v0))) = ((v1 "\/" v2) "/\" (v1 "\/" v0)) "/\" (v0 "\/" (v1 "\/" v2))

proof

let v0, v2, v1 be Element of L; :: thesis:
v1 "\/" ((v1 "\/" v2) "/\" v0) = (v1 "\/" v2) "/\" (v1 "\/" v0) by A913;
hence (v0 "/\" (v1 "\/" v2)) "\/" (v1 "/\" (v1 "\/" ((v1 "/\" v2) "\/" v0))) = ((v1 "\/" v2) "/\" (v1 "\/" v0)) "/\" (v0 "\/" (v1 "\/" v2)) by A704; :: thesis:

end;

A925: for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v1 "/\" (v1 "\/" ((v1 "/\" v2) "\/" v0))) = (v1 "\/" v2) "/\" ((v1 "\/" v0) "/\" (v0 "\/" (v1 "\/" v2)))

proof

let v0, v2, v1 be Element of L; :: thesis:
((v1 "\/" v2) "/\" (v1 "\/" v0)) "/\" (v0 "\/" (v1 "\/" v2)) = (v1 "\/" v2) "/\" ((v1 "\/" v0) "/\" (v0 "\/" (v1 "\/" v2))) by A3;
hence (v0 "/\" (v1 "\/" v2)) "\/" (v1 "/\" (v1 "\/" ((v1 "/\" v2) "\/" v0))) = (v1 "\/" v2) "/\" ((v1 "\/" v0) "/\" (v0 "\/" (v1 "\/" v2))) by A923; :: thesis:

end;

A927: for v0, v2, v1 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" (v2 "\/" ((v1 "/\" v2) "\/" v0))) = (v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v2 "\/" (v0 "\/" v1))

proof

let v0, v2, v1 be Element of L; :: thesis:
v2 "\/" ((v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v0 "\/" v1)) = (v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v2 "\/" (v0 "\/" v1)) by A913;
hence (v0 "/\" v1) "\/" (v2 "/\" (v2 "\/" ((v1 "/\" v2) "\/" v0))) = (v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v2 "\/" (v0 "\/" v1)) by A669; :: thesis:

end;

A929: for v2, v1, v0 being Element of L holds ((v0 "/\" v1) "\/" v2) "/\" ((v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v0 "\/" v1)) = (v2 "\/" ((v2 "\/" v1) "/\" v0)) "/\" (v0 "\/" v1)

proof

let v2, v1, v0 be Element of L; :: thesis:
v1 "\/" v2 = v2 "\/" v1 by A8;
hence ((v0 "/\" v1) "\/" v2) "/\" ((v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v0 "\/" v1)) = (v2 "\/" ((v2 "\/" v1) "/\" v0)) "/\" (v0 "\/" v1) by A110; :: thesis:

end;

A931: for v0, v2, v1 being Element of L holds (v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v0 "\/" v1) = (v2 "\/" ((v2 "\/" v1) "/\" v0)) "/\" (v0 "\/" v1)

proof

let v0, v2, v1 be Element of L; :: thesis:
((v0 "/\" v1) "\/" v2) "/\" ((v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v0 "\/" v1)) = (v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v0 "\/" v1) by A110;
hence (v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v0 "\/" v1) = (v2 "\/" ((v2 "\/" v1) "/\" v0)) "/\" (v0 "\/" v1) by A929; :: thesis:

end;

A934: for v2, v0, v1 being Element of L holds (v0 "\/" ((v1 "\/" v0) "/\" v2)) "/\" (v2 "\/" v1) = ((v0 "\/" v1) "/\" (v0 "\/" v2)) "/\" (v2 "\/" v1)

proof

let v2, v0, v1 be Element of L; :: thesis:
v0 "\/" ((v0 "\/" v1) "/\" v2) = (v0 "\/" v1) "/\" (v0 "\/" v2) by A913;
hence (v0 "\/" ((v1 "\/" v0) "/\" v2)) "/\" (v2 "\/" v1) = ((v0 "\/" v1) "/\" (v0 "\/" v2)) "/\" (v2 "\/" v1) by A931; :: thesis:

end;

A936: for v2, v0, v1 being Element of L holds (v0 "\/" ((v1 "\/" v0) "/\" v2)) "/\" (v2 "\/" v1) = (v0 "\/" v1) "/\" ((v0 "\/" v2) "/\" (v2 "\/" v1))

proof

let v2, v0, v1 be Element of L; :: thesis:
((v0 "\/" v1) "/\" (v0 "\/" v2)) "/\" (v2 "\/" v1) = (v0 "\/" v1) "/\" ((v0 "\/" v2) "/\" (v2 "\/" v1)) by A3;
hence (v0 "\/" ((v1 "\/" v0) "/\" v2)) "/\" (v2 "\/" v1) = (v0 "\/" v1) "/\" ((v0 "\/" v2) "/\" (v2 "\/" v1)) by A934; :: thesis:

end;

A938: for v2, v1, v0 being Element of L holds ((v0 "/\" v1) "\/" v2) "/\" ((v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v0 "\/" v1)) = (((v1 "\/" v2) "/\" v0) "\/" v2) "/\" (v0 "\/" v1)

proof

let v2, v1, v0 be Element of L; :: thesis:
v2 "\/" ((v1 "\/" v2) "/\" v0) = ((v1 "\/" v2) "/\" v0) "\/" v2 by A8;
hence ((v0 "/\" v1) "\/" v2) "/\" ((v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v0 "\/" v1)) = (((v1 "\/" v2) "/\" v0) "\/" v2) "/\" (v0 "\/" v1) by A110; :: thesis:

end;

A940: for v2, v1, v0 being Element of L holds ((v0 "/\" v1) "\/" v2) "/\" ((v2 "\/" v1) "/\" ((v2 "\/" v0) "/\" (v0 "\/" v1))) = (((v1 "\/" v2) "/\" v0) "\/" v2) "/\" (v0 "\/" v1)

proof

let v2, v1, v0 be Element of L; :: thesis:
(v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v0 "\/" v1) = (v2 "\/" v1) "/\" ((v2 "\/" v0) "/\" (v0 "\/" v1)) by A936;
hence ((v0 "/\" v1) "\/" v2) "/\" ((v2 "\/" v1) "/\" ((v2 "\/" v0) "/\" (v0 "\/" v1))) = (((v1 "\/" v2) "/\" v0) "\/" v2) "/\" (v0 "\/" v1) by A938; :: thesis:

end;

A942: for v2, v1, v0 being Element of L holds ((v0 "/\" v1) "\/" v2) "/\" ((v2 "\/" v1) "/\" ((v2 "\/" v0) "/\" (v0 "\/" v1))) = (v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v0 "\/" v1)

proof

let v2, v1, v0 be Element of L; :: thesis:
((v1 "\/" v2) "/\" v0) "\/" v2 = v2 "\/" ((v1 "\/" v2) "/\" v0) by A8;
hence ((v0 "/\" v1) "\/" v2) "/\" ((v2 "\/" v1) "/\" ((v2 "\/" v0) "/\" (v0 "\/" v1))) = (v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v0 "\/" v1) by A940; :: thesis:

end;

A944: for v2, v1, v0 being Element of L holds ((v0 "/\" v1) "\/" v2) "/\" ((v2 "\/" v1) "/\" ((v2 "\/" v0) "/\" (v0 "\/" v1))) = (v2 "\/" v1) "/\" ((v2 "\/" v0) "/\" (v0 "\/" v1))

proof

let v2, v1, v0 be Element of L; :: thesis:
(v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v0 "\/" v1) = (v2 "\/" v1) "/\" ((v2 "\/" v0) "/\" (v0 "\/" v1)) by A936;
hence ((v0 "/\" v1) "\/" v2) "/\" ((v2 "\/" v1) "/\" ((v2 "\/" v0) "/\" (v0 "\/" v1))) = (v2 "\/" v1) "/\" ((v2 "\/" v0) "/\" (v0 "\/" v1)) by A942; :: thesis:

end;

A947: for v100, v1, v0 being Element of L holds (v100 "\/" (v0 "/\" v1)) "/\" ((v100 "\/" ((v1 "\/" v100) "/\" v0)) "/\" (v0 "\/" v1)) = ((v0 "/\" v1) "\/" v100) "/\" ((v100 "\/" ((v1 "\/" v100) "/\" v0)) "/\" (v0 "\/" v1))

proof

let v100, v1, v0 be Element of L; :: thesis:
((v0 "/\" v1) "\/" v100) "/\" ((v100 "\/" ((v1 "\/" v100) "/\" v0)) "/\" (v0 "\/" v1)) = (v100 "\/" ((v1 "\/" v100) "/\" v0)) "/\" (v0 "\/" v1) by A110;
hence (v100 "\/" (v0 "/\" v1)) "/\" ((v100 "\/" ((v1 "\/" v100) "/\" v0)) "/\" (v0 "\/" v1)) = ((v0 "/\" v1) "\/" v100) "/\" ((v100 "\/" ((v1 "\/" v100) "/\" v0)) "/\" (v0 "\/" v1)) by A392; :: thesis:

end;

A950: for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" ((v0 "\/" v2) "/\" ((v0 "\/" v1) "/\" (v1 "\/" v2))) = ((v1 "/\" v2) "\/" v0) "/\" ((v0 "\/" ((v2 "\/" v0) "/\" v1)) "/\" (v1 "\/" v2))

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "\/" ((v2 "\/" v0) "/\" v1)) "/\" (v1 "\/" v2) = (v0 "\/" v2) "/\" ((v0 "\/" v1) "/\" (v1 "\/" v2)) by A936;
hence (v0 "\/" (v1 "/\" v2)) "/\" ((v0 "\/" v2) "/\" ((v0 "\/" v1) "/\" (v1 "\/" v2))) = ((v1 "/\" v2) "\/" v0) "/\" ((v0 "\/" ((v2 "\/" v0) "/\" v1)) "/\" (v1 "\/" v2)) by A947; :: thesis:

end;

A952: for v0, v2, v1 being Element of L holds (v0 "\/" v2) "/\" ((v0 "\/" (v1 "/\" v2)) "/\" ((v0 "\/" v1) "/\" (v1 "\/" v2))) = ((v1 "/\" v2) "\/" v0) "/\" ((v0 "\/" ((v2 "\/" v0) "/\" v1)) "/\" (v1 "\/" v2))

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "\/" (v1 "/\" v2)) "/\" ((v0 "\/" v2) "/\" ((v0 "\/" v1) "/\" (v1 "\/" v2))) = (v0 "\/" v2) "/\" ((v0 "\/" (v1 "/\" v2)) "/\" ((v0 "\/" v1) "/\" (v1 "\/" v2))) by A40;
hence (v0 "\/" v2) "/\" ((v0 "\/" (v1 "/\" v2)) "/\" ((v0 "\/" v1) "/\" (v1 "\/" v2))) = ((v1 "/\" v2) "\/" v0) "/\" ((v0 "\/" ((v2 "\/" v0) "/\" v1)) "/\" (v1 "\/" v2)) by A950; :: thesis:

end;

A955: for v0, v1, v2 being Element of L holds (v0 "\/" v1) "/\" ((v0 "\/" v2) "/\" ((v0 "\/" (v2 "/\" v1)) "/\" (v2 "\/" v1))) = ((v2 "/\" v1) "\/" v0) "/\" ((v0 "\/" ((v1 "\/" v0) "/\" v2)) "/\" (v2 "\/" v1))

proof

let v0, v1, v2 be Element of L; :: thesis:
(v0 "\/" (v2 "/\" v1)) "/\" ((v0 "\/" v2) "/\" (v2 "\/" v1)) = (v0 "\/" v2) "/\" ((v0 "\/" (v2 "/\" v1)) "/\" (v2 "\/" v1)) by A40;
hence (v0 "\/" v1) "/\" ((v0 "\/" v2) "/\" ((v0 "\/" (v2 "/\" v1)) "/\" (v2 "\/" v1))) = ((v2 "/\" v1) "\/" v0) "/\" ((v0 "\/" ((v1 "\/" v0) "/\" v2)) "/\" (v2 "\/" v1)) by A952; :: thesis:

end;

A957: for v0, v1, v2 being Element of L holds (v0 "\/" v1) "/\" ((v0 "\/" (v2 "/\" v1)) "/\" (v2 "\/" v1)) = ((v2 "/\" v1) "\/" v0) "/\" ((v0 "\/" ((v1 "\/" v0) "/\" v2)) "/\" (v2 "\/" v1))

proof

let v0, v1, v2 be Element of L; :: thesis:
(v0 "\/" v2) "/\" ((v0 "\/" (v2 "/\" v1)) "/\" (v2 "\/" v1)) = (v0 "\/" (v2 "/\" v1)) "/\" (v2 "\/" v1) by A60;
hence (v0 "\/" v1) "/\" ((v0 "\/" (v2 "/\" v1)) "/\" (v2 "\/" v1)) = ((v2 "/\" v1) "\/" v0) "/\" ((v0 "\/" ((v1 "\/" v0) "/\" v2)) "/\" (v2 "\/" v1)) by A955; :: thesis:

end;

A959: for v0, v1, v2 being Element of L holds (v0 "\/" (v2 "/\" v1)) "/\" (v2 "\/" v1) = ((v2 "/\" v1) "\/" v0) "/\" ((v0 "\/" ((v1 "\/" v0) "/\" v2)) "/\" (v2 "\/" v1))

proof

let v0, v1, v2 be Element of L; :: thesis:
(v0 "\/" v1) "/\" ((v0 "\/" (v2 "/\" v1)) "/\" (v2 "\/" v1)) = (v0 "\/" (v2 "/\" v1)) "/\" (v2 "\/" v1) by A315;
hence (v0 "\/" (v2 "/\" v1)) "/\" (v2 "\/" v1) = ((v2 "/\" v1) "\/" v0) "/\" ((v0 "\/" ((v1 "\/" v0) "/\" v2)) "/\" (v2 "\/" v1)) by A957; :: thesis:

end;

A962: for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v1 "\/" v2) = ((v1 "/\" v2) "\/" v0) "/\" ((v0 "\/" v2) "/\" ((v0 "\/" v1) "/\" (v1 "\/" v2)))

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "\/" ((v2 "\/" v0) "/\" v1)) "/\" (v1 "\/" v2) = (v0 "\/" v2) "/\" ((v0 "\/" v1) "/\" (v1 "\/" v2)) by A936;
hence (v0 "\/" (v1 "/\" v2)) "/\" (v1 "\/" v2) = ((v1 "/\" v2) "\/" v0) "/\" ((v0 "\/" v2) "/\" ((v0 "\/" v1) "/\" (v1 "\/" v2))) by A959; :: thesis:

end;

A964: for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v1 "\/" v2) = (v0 "\/" v2) "/\" ((v0 "\/" v1) "/\" (v1 "\/" v2))

proof

let v0, v2, v1 be Element of L; :: thesis:
((v1 "/\" v2) "\/" v0) "/\" ((v0 "\/" v2) "/\" ((v0 "\/" v1) "/\" (v1 "\/" v2))) = (v0 "\/" v2) "/\" ((v0 "\/" v1) "/\" (v1 "\/" v2)) by A944;
hence (v0 "\/" (v1 "/\" v2)) "/\" (v1 "\/" v2) = (v0 "\/" v2) "/\" ((v0 "\/" v1) "/\" (v1 "\/" v2)) by A962; :: thesis:

end;

A966: for v1, v2, v0 being Element of L holds (v0 "\/" (v0 "\/" v2)) "/\" ((v0 "\/" v1) "/\" (v1 "\/" (v0 "\/" v2))) = v0 "\/" (v1 "/\" (v0 "\/" v2))

proof

let v1, v2, v0 be Element of L; :: thesis:
(v0 "\/" (v1 "/\" (v0 "\/" v2))) "/\" (v1 "\/" (v0 "\/" v2)) = (v0 "\/" (v0 "\/" v2)) "/\" ((v0 "\/" v1) "/\" (v1 "\/" (v0 "\/" v2))) by A964;
hence (v0 "\/" (v0 "\/" v2)) "/\" ((v0 "\/" v1) "/\" (v1 "\/" (v0 "\/" v2))) = v0 "\/" (v1 "/\" (v0 "\/" v2)) by A902; :: thesis:

end;

A969: for v2, v1, v0 being Element of L holds (v0 "\/" v1) "/\" ((v0 "\/" v2) "/\" (v2 "\/" (v0 "\/" v1))) = v0 "\/" (v2 "/\" (v0 "\/" v1))

proof

let v2, v1, v0 be Element of L; :: thesis:
v0 "\/" (v0 "\/" v1) = v0 "\/" v1 by A43;
hence (v0 "\/" v1) "/\" ((v0 "\/" v2) "/\" (v2 "\/" (v0 "\/" v1))) = v0 "\/" (v2 "/\" (v0 "\/" v1)) by A966; :: thesis:

end;

A974: for v1, v101, v100 being Element of L holds v100 "\/" ((v100 "/\" v101) "/\" ((v100 "/\" v101) "\/" v1)) = ((v100 "/\" v101) "/\" v1) "\/" (v100 "/\" (v100 "\/" v101))

proof

let v1, v101, v100 be Element of L; :: thesis:
(v100 "/\" v101) "\/" ((v100 "/\" v101) "/\" v1) = (v100 "/\" v101) "/\" ((v100 "/\" v101) "\/" v1) by A347;
hence v100 "\/" ((v100 "/\" v101) "/\" ((v100 "/\" v101) "\/" v1)) = ((v100 "/\" v101) "/\" v1) "\/" (v100 "/\" (v100 "\/" v101)) by A603; :: thesis:

end;

A977: for v2, v1, v0 being Element of L holds v0 "\/" (v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2))) = ((v0 "/\" v1) "/\" v2) "\/" (v0 "/\" (v0 "\/" v1))

proof

let v2, v1, v0 be Element of L; :: thesis:
(v0 "/\" v1) "/\" ((v0 "/\" v1) "\/" v2) = v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2)) by A3;
hence v0 "\/" (v0 "/\" (v1 "/\" ((v0 "/\" v1) "\/" v2))) = ((v0 "/\" v1) "/\" v2) "\/" (v0 "/\" (v0 "\/" v1)) by A974; :: thesis:

end;

A979: for v2, v1, v0 being Element of L holds v0 "\/" (v1 "/\" (v0 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "\/" (v1 "/\" v2))))) = ((v0 "/\" v1) "/\" v2) "\/" (v0 "/\" (v0 "\/" v1))

proof

end;

A981: for v2, v1, v0 being Element of L holds v0 "/\" (v0 "\/" (v1 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "\/" (v1 "/\" v2))))) = ((v0 "/\" v1) "/\" v2) "\/" (v0 "/\" (v0 "\/" v1))

proof

end;

A983: for v0, v1, v2 being Element of L holds v0 "/\" (v0 "\/" (v2 "/\" v1)) = ((v0 "/\" v1) "/\" v2) "\/" (v0 "/\" (v0 "\/" v1))

proof

let v0, v1, v2 be Element of L; :: thesis:
v0 "/\" (v0 "\/" (v1 "/\" ((v1 "\/" (v0 "/\" ((v0 "\/" v1) "/\" v2))) "/\" (v0 "\/" (v1 "/\" v2))))) = v0 "/\" (v0 "\/" (v2 "/\" v1)) by A878;
hence v0 "/\" (v0 "\/" (v2 "/\" v1)) = ((v0 "/\" v1) "/\" v2) "\/" (v0 "/\" (v0 "\/" v1)) by A981; :: thesis:

end;

A986: for v0, v2, v1 being Element of L holds v0 "/\" (v0 "\/" (v1 "/\" v2)) = (v0 "/\" (v2 "/\" v1)) "\/" (v0 "/\" (v0 "\/" v2))

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "/\" v2) "/\" v1 = v0 "/\" (v2 "/\" v1) by A3;
hence v0 "/\" (v0 "\/" (v1 "/\" v2)) = (v0 "/\" (v2 "/\" v1)) "\/" (v0 "/\" (v0 "\/" v2)) by A983; :: thesis:

end;

A991: for v100, v1, v102 being Element of L holds v100 "\/" (v102 "\/" ((v102 "/\" v1) "\/" (v100 "/\" (v102 "\/" v1)))) = v100 "\/" (v102 "/\" (v102 "\/" v1))

proof

let v100, v1, v102 be Element of L; :: thesis:
v102 "\/" ((v102 "/\" v1) "\/" (v100 "/\" (v102 "\/" v1))) = (v100 "/\" (v102 "\/" v1)) "\/" (v102 "/\" (v102 "\/" v1)) by A603;
hence v100 "\/" (v102 "\/" ((v102 "/\" v1) "\/" (v100 "/\" (v102 "\/" v1)))) = v100 "\/" (v102 "/\" (v102 "\/" v1)) by A558; :: thesis:

end;

A994: for v0, v2, v1 being Element of L holds v0 "\/" (v1 "\/" (v0 "/\" (v1 "\/" v2))) = v0 "\/" (v1 "/\" (v1 "\/" v2))

proof

let v0, v2, v1 be Element of L; :: thesis:
v1 "\/" ((v1 "/\" v2) "\/" (v0 "/\" (v1 "\/" v2))) = v1 "\/" (v0 "/\" (v1 "\/" v2)) by A884;
hence v0 "\/" (v1 "\/" (v0 "/\" (v1 "\/" v2))) = v0 "\/" (v1 "/\" (v1 "\/" v2)) by A991; :: thesis:

end;

A996: for v0, v2, v1 being Element of L holds (v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" (v1 "\/" v2))) = v0 "\/" (v1 "/\" (v1 "\/" v2))

proof

let v0, v2, v1 be Element of L; :: thesis:
v0 "\/" (v1 "\/" (v0 "/\" (v1 "\/" v2))) = (v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" (v1 "\/" v2))) by A776;
hence (v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" (v1 "\/" v2))) = v0 "\/" (v1 "/\" (v1 "\/" v2)) by A994; :: thesis:

end;

A998: for v0, v2, v1 being Element of L holds (v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" v2)) = v0 "\/" (v1 "/\" (v1 "\/" v2))

proof

let v0, v2, v1 be Element of L; :: thesis:
v1 "\/" (v1 "\/" v2) = v1 "\/" v2 by A43;
hence (v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" v2)) = v0 "\/" (v1 "/\" (v1 "\/" v2)) by A996; :: thesis:

end;

A1001: for v0, v2, v1 being Element of L holds ((v0 "/\" (v1 "/\" v2)) "\/" v0) "/\" ((v0 "/\" (v1 "/\" v2)) "\/" (v0 "\/" v1)) = v0 "/\" (v0 "\/" (v2 "/\" v1))

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "/\" (v1 "/\" v2)) "\/" (v0 "/\" (v0 "\/" v1)) = ((v0 "/\" (v1 "/\" v2)) "\/" v0) "/\" ((v0 "/\" (v1 "/\" v2)) "\/" (v0 "\/" v1)) by A998;
hence ((v0 "/\" (v1 "/\" v2)) "\/" v0) "/\" ((v0 "/\" (v1 "/\" v2)) "\/" (v0 "\/" v1)) = v0 "/\" (v0 "\/" (v2 "/\" v1)) by A986; :: thesis:

end;

A1003: for v0, v2, v1 being Element of L holds (v0 "\/" (v0 "/\" (v1 "/\" v2))) "/\" ((v0 "/\" (v1 "/\" v2)) "\/" (v0 "\/" v1)) = v0 "/\" (v0 "\/" (v2 "/\" v1))

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "/\" (v1 "/\" v2)) "\/" v0 = v0 "\/" (v0 "/\" (v1 "/\" v2)) by A8;
hence (v0 "\/" (v0 "/\" (v1 "/\" v2))) "/\" ((v0 "/\" (v1 "/\" v2)) "\/" (v0 "\/" v1)) = v0 "/\" (v0 "\/" (v2 "/\" v1)) by A1001; :: thesis:

end;

A1005: for v0, v2, v1 being Element of L holds (v0 "/\" (v0 "\/" (v1 "/\" v2))) "/\" ((v0 "/\" (v1 "/\" v2)) "\/" (v0 "\/" v1)) = v0 "/\" (v0 "\/" (v2 "/\" v1))

proof

let v0, v2, v1 be Element of L; :: thesis:
v0 "\/" (v0 "/\" (v1 "/\" v2)) = v0 "/\" (v0 "\/" (v1 "/\" v2)) by A347;
hence (v0 "/\" (v0 "\/" (v1 "/\" v2))) "/\" ((v0 "/\" (v1 "/\" v2)) "\/" (v0 "\/" v1)) = v0 "/\" (v0 "\/" (v2 "/\" v1)) by A1003; :: thesis:

end;

A1007: for v0, v2, v1 being Element of L holds (v0 "/\" (v0 "\/" (v1 "/\" v2))) "/\" (v0 "\/" ((v0 "/\" (v1 "/\" v2)) "\/" v1)) = v0 "/\" (v0 "\/" (v2 "/\" v1))

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "/\" (v1 "/\" v2)) "\/" (v0 "\/" v1) = v0 "\/" ((v0 "/\" (v1 "/\" v2)) "\/" v1) by A57;
hence (v0 "/\" (v0 "\/" (v1 "/\" v2))) "/\" (v0 "\/" ((v0 "/\" (v1 "/\" v2)) "\/" v1)) = v0 "/\" (v0 "\/" (v2 "/\" v1)) by A1005; :: thesis:

end;

A1009: for v0, v2, v1 being Element of L holds (v0 "/\" (v0 "\/" (v1 "/\" v2))) "/\" (v0 "\/" (v1 "\/" (v0 "/\" (v1 "/\" v2)))) = v0 "/\" (v0 "\/" (v2 "/\" v1))

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "/\" (v1 "/\" v2)) "\/" v1 = v1 "\/" (v0 "/\" (v1 "/\" v2)) by A8;
hence (v0 "/\" (v0 "\/" (v1 "/\" v2))) "/\" (v0 "\/" (v1 "\/" (v0 "/\" (v1 "/\" v2)))) = v0 "/\" (v0 "\/" (v2 "/\" v1)) by A1007; :: thesis:

end;

A1011: for v0, v2, v1 being Element of L holds (v0 "/\" (v0 "\/" (v1 "/\" v2))) "/\" (v0 "\/" (v1 "/\" (v1 "\/" (v0 "/\" v2)))) = v0 "/\" (v0 "\/" (v2 "/\" v1))

proof

let v0, v2, v1 be Element of L; :: thesis:
v1 "\/" (v0 "/\" (v1 "/\" v2)) = v1 "/\" (v1 "\/" (v0 "/\" v2)) by A417;
hence (v0 "/\" (v0 "\/" (v1 "/\" v2))) "/\" (v0 "\/" (v1 "/\" (v1 "\/" (v0 "/\" v2)))) = v0 "/\" (v0 "\/" (v2 "/\" v1)) by A1009; :: thesis:

end;

A1013: for v0, v2, v1 being Element of L holds (v0 "/\" (v0 "\/" (v1 "/\" v2))) "/\" ((v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" (v0 "/\" v2)))) = v0 "/\" (v0 "\/" (v2 "/\" v1))

proof

let v0, v2, v1 be Element of L; :: thesis:
v0 "\/" (v1 "/\" (v1 "\/" (v0 "/\" v2))) = (v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" (v0 "/\" v2))) by A998;
hence (v0 "/\" (v0 "\/" (v1 "/\" v2))) "/\" ((v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" (v0 "/\" v2)))) = v0 "/\" (v0 "\/" (v2 "/\" v1)) by A1011; :: thesis:

end;

A1015: for v0, v2, v1 being Element of L holds (v0 "/\" (v0 "\/" (v1 "/\" v2))) "/\" ((v0 "\/" v1) "/\" ((v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" v2)))) = v0 "/\" (v0 "\/" (v2 "/\" v1))

proof

let v0, v2, v1 be Element of L; :: thesis:
v0 "\/" (v1 "\/" (v0 "/\" v2)) = (v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" v2)) by A776;
hence (v0 "/\" (v0 "\/" (v1 "/\" v2))) "/\" ((v0 "\/" v1) "/\" ((v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" v2)))) = v0 "/\" (v0 "\/" (v2 "/\" v1)) by A1013; :: thesis:

end;

A1017: for v0, v2, v1 being Element of L holds (v0 "/\" (v0 "\/" (v1 "/\" v2))) "/\" ((v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" v2))) = v0 "/\" (v0 "\/" (v2 "/\" v1))

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "\/" v1) "/\" ((v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" v2))) = (v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" v2)) by A26;
hence (v0 "/\" (v0 "\/" (v1 "/\" v2))) "/\" ((v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" v2))) = v0 "/\" (v0 "\/" (v2 "/\" v1)) by A1015; :: thesis:

end;

A1019: for v0, v2, v1 being Element of L holds (v0 "\/" v1) "/\" ((v0 "/\" (v0 "\/" (v1 "/\" v2))) "/\" (v0 "\/" (v1 "\/" v2))) = v0 "/\" (v0 "\/" (v2 "/\" v1))

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "/\" (v0 "\/" (v1 "/\" v2))) "/\" ((v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" v2))) = (v0 "\/" v1) "/\" ((v0 "/\" (v0 "\/" (v1 "/\" v2))) "/\" (v0 "\/" (v1 "\/" v2))) by A40;
hence (v0 "\/" v1) "/\" ((v0 "/\" (v0 "\/" (v1 "/\" v2))) "/\" (v0 "\/" (v1 "\/" v2))) = v0 "/\" (v0 "\/" (v2 "/\" v1)) by A1017; :: thesis:

end;

A1021: for v0, v2, v1 being Element of L holds (v0 "\/" v1) "/\" (v0 "/\" ((v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" (v1 "\/" v2)))) = v0 "/\" (v0 "\/" (v2 "/\" v1))

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "/\" (v0 "\/" (v1 "/\" v2))) "/\" (v0 "\/" (v1 "\/" v2)) = v0 "/\" ((v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" (v1 "\/" v2))) by A3;
hence (v0 "\/" v1) "/\" (v0 "/\" ((v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" (v1 "\/" v2)))) = v0 "/\" (v0 "\/" (v2 "/\" v1)) by A1019; :: thesis:

end;

A1023: for v0, v2, v1 being Element of L holds (v0 "\/" v1) "/\" (v0 "/\" (v0 "\/" (v1 "\/" v2))) = v0 "/\" (v0 "\/" (v2 "/\" v1))

proof

let v0, v2, v1 be Element of L; :: thesis:
v0 "/\" ((v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" (v1 "\/" v2))) = v0 "/\" (v0 "\/" (v1 "\/" v2)) by A735;
hence (v0 "\/" v1) "/\" (v0 "/\" (v0 "\/" (v1 "\/" v2))) = v0 "/\" (v0 "\/" (v2 "/\" v1)) by A1021; :: thesis:

end;

A1025: for v0, v2, v1 being Element of L holds v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" v2))) = v0 "/\" (v0 "\/" (v2 "/\" v1))

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "\/" v1) "/\" (v0 "/\" (v0 "\/" (v1 "\/" v2))) = v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" v2))) by A40;
hence v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" v2))) = v0 "/\" (v0 "\/" (v2 "/\" v1)) by A1023; :: thesis:

end;

A1027: for v0, v2, v1 being Element of L holds v0 "/\" (v0 "\/" (v1 "\/" v2)) = v0 "/\" (v0 "\/" (v2 "/\" v1))

proof

let v0, v2, v1 be Element of L; :: thesis:
v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" v2))) = v0 "/\" (v0 "\/" (v1 "\/" v2)) by A600;
hence v0 "/\" (v0 "\/" (v1 "\/" v2)) = v0 "/\" (v0 "\/" (v2 "/\" v1)) by A1025; :: thesis:

end;

A1029: for v0, v2, v1 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" (v2 "\/" (v0 "/\" (v1 "/\" v2)))) = (v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v2 "\/" (v0 "\/" v1))

proof

let v0, v2, v1 be Element of L; :: thesis:
v2 "/\" (v2 "\/" ((v1 "/\" v2) "\/" v0)) = v2 "/\" (v2 "\/" (v0 "/\" (v1 "/\" v2))) by A1027;
hence (v0 "/\" v1) "\/" (v2 "/\" (v2 "\/" (v0 "/\" (v1 "/\" v2)))) = (v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v2 "\/" (v0 "\/" v1)) by A927; :: thesis:

end;

A1031: for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" (v2 "/\" (v2 "\/" (v0 "/\" v1)))) = (v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v2 "\/" (v0 "\/" v1))

proof

let v2, v1, v0 be Element of L; :: thesis:
v2 "\/" (v0 "/\" (v1 "/\" v2)) = v2 "/\" (v2 "\/" (v0 "/\" v1)) by A441;
hence (v0 "/\" v1) "\/" (v2 "/\" (v2 "/\" (v2 "\/" (v0 "/\" v1)))) = (v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v2 "\/" (v0 "\/" v1)) by A1029; :: thesis:

end;

A1033: for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" (v2 "\/" (v0 "/\" v1))) = (v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v2 "\/" (v0 "\/" v1))

proof

let v2, v1, v0 be Element of L; :: thesis:
v2 "/\" (v2 "/\" (v2 "\/" (v0 "/\" v1))) = v2 "/\" (v2 "\/" (v0 "/\" v1)) by A26;
hence (v0 "/\" v1) "\/" (v2 "/\" (v2 "\/" (v0 "/\" v1))) = (v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v2 "\/" (v0 "\/" v1)) by A1031; :: thesis:

end;

A1035: for v2, v1, v0 being Element of L holds v2 "\/" (v0 "/\" v1) = (v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v2 "\/" (v0 "\/" v1))

proof

let v2, v1, v0 be Element of L; :: thesis:
(v0 "/\" v1) "\/" (v2 "/\" (v2 "\/" (v0 "/\" v1))) = v2 "\/" (v0 "/\" v1) by A344;
hence v2 "\/" (v0 "/\" v1) = (v2 "\/" ((v1 "\/" v2) "/\" v0)) "/\" (v2 "\/" (v0 "\/" v1)) by A1033; :: thesis:

end;

A1040: for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v1 "/\" (v1 "\/" (v0 "/\" (v1 "/\" v2)))) = (v1 "\/" v2) "/\" ((v1 "\/" v0) "/\" (v0 "\/" (v1 "\/" v2)))

proof

let v0, v2, v1 be Element of L; :: thesis:
v1 "/\" (v1 "\/" ((v1 "/\" v2) "\/" v0)) = v1 "/\" (v1 "\/" (v0 "/\" (v1 "/\" v2))) by A1027;
hence (v0 "/\" (v1 "\/" v2)) "\/" (v1 "/\" (v1 "\/" (v0 "/\" (v1 "/\" v2)))) = (v1 "\/" v2) "/\" ((v1 "\/" v0) "/\" (v0 "\/" (v1 "\/" v2))) by A925; :: thesis:

end;

A1042: for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v1 "/\" (v1 "/\" (v1 "\/" (v0 "/\" v2)))) = (v1 "\/" v2) "/\" ((v1 "\/" v0) "/\" (v0 "\/" (v1 "\/" v2)))

proof

let v0, v2, v1 be Element of L; :: thesis:
v1 "\/" (v0 "/\" (v1 "/\" v2)) = v1 "/\" (v1 "\/" (v0 "/\" v2)) by A417;
hence (v0 "/\" (v1 "\/" v2)) "\/" (v1 "/\" (v1 "/\" (v1 "\/" (v0 "/\" v2)))) = (v1 "\/" v2) "/\" ((v1 "\/" v0) "/\" (v0 "\/" (v1 "\/" v2))) by A1040; :: thesis:

end;

A1044: for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v1 "/\" (v1 "\/" (v0 "/\" v2))) = (v1 "\/" v2) "/\" ((v1 "\/" v0) "/\" (v0 "\/" (v1 "\/" v2)))

proof

let v0, v2, v1 be Element of L; :: thesis:
v1 "/\" (v1 "/\" (v1 "\/" (v0 "/\" v2))) = v1 "/\" (v1 "\/" (v0 "/\" v2)) by A26;
hence (v0 "/\" (v1 "\/" v2)) "\/" (v1 "/\" (v1 "\/" (v0 "/\" v2))) = (v1 "\/" v2) "/\" ((v1 "\/" v0) "/\" (v0 "\/" (v1 "\/" v2))) by A1042; :: thesis:

end;

A1046: for v0, v2, v1 being Element of L holds ((v0 "/\" (v1 "\/" v2)) "\/" v1) "/\" ((v0 "/\" (v1 "\/" v2)) "\/" (v1 "\/" (v0 "/\" v2))) = (v1 "\/" v2) "/\" ((v1 "\/" v0) "/\" (v0 "\/" (v1 "\/" v2)))

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "/\" (v1 "\/" v2)) "\/" (v1 "/\" (v1 "\/" (v0 "/\" v2))) = ((v0 "/\" (v1 "\/" v2)) "\/" v1) "/\" ((v0 "/\" (v1 "\/" v2)) "\/" (v1 "\/" (v0 "/\" v2))) by A998;
hence ((v0 "/\" (v1 "\/" v2)) "\/" v1) "/\" ((v0 "/\" (v1 "\/" v2)) "\/" (v1 "\/" (v0 "/\" v2))) = (v1 "\/" v2) "/\" ((v1 "\/" v0) "/\" (v0 "\/" (v1 "\/" v2))) by A1044; :: thesis:

end;

A1048: for v0, v2, v1 being Element of L holds (v1 "\/" (v0 "/\" (v1 "\/" v2))) "/\" ((v0 "/\" (v1 "\/" v2)) "\/" (v1 "\/" (v0 "/\" v2))) = (v1 "\/" v2) "/\" ((v1 "\/" v0) "/\" (v0 "\/" (v1 "\/" v2)))

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "/\" (v1 "\/" v2)) "\/" v1 = v1 "\/" (v0 "/\" (v1 "\/" v2)) by A8;
hence (v1 "\/" (v0 "/\" (v1 "\/" v2))) "/\" ((v0 "/\" (v1 "\/" v2)) "\/" (v1 "\/" (v0 "/\" v2))) = (v1 "\/" v2) "/\" ((v1 "\/" v0) "/\" (v0 "\/" (v1 "\/" v2))) by A1046; :: thesis:

end;

A1051: for v1, v2, v0 being Element of L holds (v0 "\/" (v1 "/\" (v0 "\/" v2))) "/\" (v0 "\/" ((v1 "/\" (v0 "\/" v2)) "\/" (v1 "/\" v2))) = (v0 "\/" v2) "/\" ((v0 "\/" v1) "/\" (v1 "\/" (v0 "\/" v2)))

proof

let v1, v2, v0 be Element of L; :: thesis:
(v1 "/\" (v0 "\/" v2)) "\/" (v0 "\/" (v1 "/\" v2)) = v0 "\/" ((v1 "/\" (v0 "\/" v2)) "\/" (v1 "/\" v2)) by A57;
hence (v0 "\/" (v1 "/\" (v0 "\/" v2))) "/\" (v0 "\/" ((v1 "/\" (v0 "\/" v2)) "\/" (v1 "/\" v2))) = (v0 "\/" v2) "/\" ((v0 "\/" v1) "/\" (v1 "\/" (v0 "\/" v2))) by A1048; :: thesis:

end;

A1053: for v1, v2, v0 being Element of L holds (v0 "\/" (v1 "/\" (v0 "\/" v2))) "/\" (v0 "\/" ((v1 "/\" v2) "\/" (v1 "/\" (v0 "\/" v2)))) = (v0 "\/" v2) "/\" ((v0 "\/" v1) "/\" (v1 "\/" (v0 "\/" v2)))

proof

let v1, v2, v0 be Element of L; :: thesis:
(v1 "/\" (v0 "\/" v2)) "\/" (v1 "/\" v2) = (v1 "/\" v2) "\/" (v1 "/\" (v0 "\/" v2)) by A8;
hence (v0 "\/" (v1 "/\" (v0 "\/" v2))) "/\" (v0 "\/" ((v1 "/\" v2) "\/" (v1 "/\" (v0 "\/" v2)))) = (v0 "\/" v2) "/\" ((v0 "\/" v1) "/\" (v1 "\/" (v0 "\/" v2))) by A1051; :: thesis:

end;

A1055: for v1, v2, v0 being Element of L holds (v0 "\/" (v1 "/\" (v0 "\/" v2))) "/\" (v0 "\/" (v1 "/\" (v2 "\/" v0))) = (v0 "\/" v2) "/\" ((v0 "\/" v1) "/\" (v1 "\/" (v0 "\/" v2)))

proof

let v1, v2, v0 be Element of L; :: thesis:
(v1 "/\" v2) "\/" (v1 "/\" (v0 "\/" v2)) = v1 "/\" (v2 "\/" v0) by A133;
hence (v0 "\/" (v1 "/\" (v0 "\/" v2))) "/\" (v0 "\/" (v1 "/\" (v2 "\/" v0))) = (v0 "\/" v2) "/\" ((v0 "\/" v1) "/\" (v1 "\/" (v0 "\/" v2))) by A1053; :: thesis:

end;

A1057: for v1, v0, v2 being Element of L holds v0 "\/" (v1 "/\" (v2 "\/" v0)) = (v0 "\/" v2) "/\" ((v0 "\/" v1) "/\" (v1 "\/" (v0 "\/" v2)))

proof

let v1, v0, v2 be Element of L; :: thesis:
(v0 "\/" (v1 "/\" (v0 "\/" v2))) "/\" (v0 "\/" (v1 "/\" (v2 "\/" v0))) = v0 "\/" (v1 "/\" (v2 "\/" v0)) by A438;
hence v0 "\/" (v1 "/\" (v2 "\/" v0)) = (v0 "\/" v2) "/\" ((v0 "\/" v1) "/\" (v1 "\/" (v0 "\/" v2))) by A1055; :: thesis:

end;

A1059: for v2, v1, v0 being Element of L holds (((v0 "\/" v1) "/\" v2) "\/" v0) "/\" (((v0 "\/" v1) "/\" v2) "\/" (v0 "\/" v2)) = v0 "\/" (v2 "/\" (v0 "\/" v1))

proof

let v2, v1, v0 be Element of L; :: thesis:
((v0 "\/" v1) "/\" v2) "\/" (v0 "/\" (v0 "\/" v2)) = (((v0 "\/" v1) "/\" v2) "\/" v0) "/\" (((v0 "\/" v1) "/\" v2) "\/" (v0 "\/" v2)) by A998;
hence (((v0 "\/" v1) "/\" v2) "\/" v0) "/\" (((v0 "\/" v1) "/\" v2) "\/" (v0 "\/" v2)) = v0 "\/" (v2 "/\" (v0 "\/" v1)) by A758; :: thesis:

end;

A1061: for v2, v1, v0 being Element of L holds (v0 "\/" ((v0 "\/" v1) "/\" v2)) "/\" (((v0 "\/" v1) "/\" v2) "\/" (v0 "\/" v2)) = v0 "\/" (v2 "/\" (v0 "\/" v1))

proof

let v2, v1, v0 be Element of L; :: thesis:
((v0 "\/" v1) "/\" v2) "\/" v0 = v0 "\/" ((v0 "\/" v1) "/\" v2) by A8;
hence (v0 "\/" ((v0 "\/" v1) "/\" v2)) "/\" (((v0 "\/" v1) "/\" v2) "\/" (v0 "\/" v2)) = v0 "\/" (v2 "/\" (v0 "\/" v1)) by A1059; :: thesis:

end;

A1063: for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" (v0 "\/" v2)) "/\" (((v0 "\/" v1) "/\" v2) "\/" (v0 "\/" v2)) = v0 "\/" (v2 "/\" (v0 "\/" v1))

proof

let v2, v1, v0 be Element of L; :: thesis:
v0 "\/" ((v0 "\/" v1) "/\" v2) = (v0 "\/" v1) "/\" (v0 "\/" v2) by A913;
hence ((v0 "\/" v1) "/\" (v0 "\/" v2)) "/\" (((v0 "\/" v1) "/\" v2) "\/" (v0 "\/" v2)) = v0 "\/" (v2 "/\" (v0 "\/" v1)) by A1061; :: thesis:

end;

A1065: for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" (v0 "\/" v2)) "/\" (v0 "\/" (((v0 "\/" v1) "/\" v2) "\/" v2)) = v0 "\/" (v2 "/\" (v0 "\/" v1))

proof

let v2, v1, v0 be Element of L; :: thesis:
((v0 "\/" v1) "/\" v2) "\/" (v0 "\/" v2) = v0 "\/" (((v0 "\/" v1) "/\" v2) "\/" v2) by A57;
hence ((v0 "\/" v1) "/\" (v0 "\/" v2)) "/\" (v0 "\/" (((v0 "\/" v1) "/\" v2) "\/" v2)) = v0 "\/" (v2 "/\" (v0 "\/" v1)) by A1063; :: thesis:

end;

A1067: for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" (v0 "\/" v2)) "/\" (v0 "\/" (v2 "\/" ((v0 "\/" v1) "/\" v2))) = v0 "\/" (v2 "/\" (v0 "\/" v1))

proof

let v2, v1, v0 be Element of L; :: thesis:
((v0 "\/" v1) "/\" v2) "\/" v2 = v2 "\/" ((v0 "\/" v1) "/\" v2) by A8;
hence ((v0 "\/" v1) "/\" (v0 "\/" v2)) "/\" (v0 "\/" (v2 "\/" ((v0 "\/" v1) "/\" v2))) = v0 "\/" (v2 "/\" (v0 "\/" v1)) by A1065; :: thesis:

end;

A1069: for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" (v0 "\/" v2)) "/\" (v0 "\/" (v2 "/\" (v2 "\/" (v0 "\/" v1)))) = v0 "\/" (v2 "/\" (v0 "\/" v1))

proof

let v2, v1, v0 be Element of L; :: thesis:
v2 "\/" ((v0 "\/" v1) "/\" v2) = v2 "/\" (v2 "\/" (v0 "\/" v1)) by A400;
hence ((v0 "\/" v1) "/\" (v0 "\/" v2)) "/\" (v0 "\/" (v2 "/\" (v2 "\/" (v0 "\/" v1)))) = v0 "\/" (v2 "/\" (v0 "\/" v1)) by A1067; :: thesis:

end;

A1071: for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" (v0 "\/" v2)) "/\" (v0 "\/" (v2 "/\" (v2 "\/" (v1 "/\" v0)))) = v0 "\/" (v2 "/\" (v0 "\/" v1))

proof

let v2, v1, v0 be Element of L; :: thesis:
v2 "/\" (v2 "\/" (v0 "\/" v1)) = v2 "/\" (v2 "\/" (v1 "/\" v0)) by A1027;
hence ((v0 "\/" v1) "/\" (v0 "\/" v2)) "/\" (v0 "\/" (v2 "/\" (v2 "\/" (v1 "/\" v0)))) = v0 "\/" (v2 "/\" (v0 "\/" v1)) by A1069; :: thesis:

end;

A1073: for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" (v0 "\/" v2)) "/\" ((v0 "\/" v2) "/\" (v0 "\/" (v2 "\/" (v1 "/\" v0)))) = v0 "\/" (v2 "/\" (v0 "\/" v1))

proof

let v2, v1, v0 be Element of L; :: thesis:
v0 "\/" (v2 "/\" (v2 "\/" (v1 "/\" v0))) = (v0 "\/" v2) "/\" (v0 "\/" (v2 "\/" (v1 "/\" v0))) by A998;
hence ((v0 "\/" v1) "/\" (v0 "\/" v2)) "/\" ((v0 "\/" v2) "/\" (v0 "\/" (v2 "\/" (v1 "/\" v0)))) = v0 "\/" (v2 "/\" (v0 "\/" v1)) by A1071; :: thesis:

end;

A1075: for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" (v0 "\/" v2)) "/\" ((v0 "\/" v2) "/\" ((v0 "\/" v2) "/\" (v0 "\/" (v2 "\/" v1)))) = v0 "\/" (v2 "/\" (v0 "\/" v1))

proof

let v2, v1, v0 be Element of L; :: thesis:
v0 "\/" (v2 "\/" (v1 "/\" v0)) = (v0 "\/" v2) "/\" (v0 "\/" (v2 "\/" v1)) by A754;
hence ((v0 "\/" v1) "/\" (v0 "\/" v2)) "/\" ((v0 "\/" v2) "/\" ((v0 "\/" v2) "/\" (v0 "\/" (v2 "\/" v1)))) = v0 "\/" (v2 "/\" (v0 "\/" v1)) by A1073; :: thesis:

end;

A1077: for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" (v0 "\/" v2)) "/\" ((v0 "\/" v2) "/\" (v0 "\/" (v2 "\/" v1))) = v0 "\/" (v2 "/\" (v0 "\/" v1))

proof

let v2, v1, v0 be Element of L; :: thesis:
(v0 "\/" v2) "/\" ((v0 "\/" v2) "/\" (v0 "\/" (v2 "\/" v1))) = (v0 "\/" v2) "/\" (v0 "\/" (v2 "\/" v1)) by A26;
hence ((v0 "\/" v1) "/\" (v0 "\/" v2)) "/\" ((v0 "\/" v2) "/\" (v0 "\/" (v2 "\/" v1))) = v0 "\/" (v2 "/\" (v0 "\/" v1)) by A1075; :: thesis:

end;

A1079: for v2, v1, v0 being Element of L holds (v0 "\/" v2) "/\" (((v0 "\/" v1) "/\" (v0 "\/" v2)) "/\" (v0 "\/" (v2 "\/" v1))) = v0 "\/" (v2 "/\" (v0 "\/" v1))

proof

let v2, v1, v0 be Element of L; :: thesis:
((v0 "\/" v1) "/\" (v0 "\/" v2)) "/\" ((v0 "\/" v2) "/\" (v0 "\/" (v2 "\/" v1))) = (v0 "\/" v2) "/\" (((v0 "\/" v1) "/\" (v0 "\/" v2)) "/\" (v0 "\/" (v2 "\/" v1))) by A40;
hence (v0 "\/" v2) "/\" (((v0 "\/" v1) "/\" (v0 "\/" v2)) "/\" (v0 "\/" (v2 "\/" v1))) = v0 "\/" (v2 "/\" (v0 "\/" v1)) by A1077; :: thesis:

end;

A1082: for v0, v2, v1 being Element of L holds (v0 "\/" v1) "/\" ((v0 "\/" v2) "/\" ((v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" v2)))) = v0 "\/" (v1 "/\" (v0 "\/" v2))

proof

let v0, v2, v1 be Element of L; :: thesis:
((v0 "\/" v2) "/\" (v0 "\/" v1)) "/\" (v0 "\/" (v1 "\/" v2)) = (v0 "\/" v2) "/\" ((v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" v2))) by A3;
hence (v0 "\/" v1) "/\" ((v0 "\/" v2) "/\" ((v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" v2)))) = v0 "\/" (v1 "/\" (v0 "\/" v2)) by A1079; :: thesis:

end;

A1084: for v0, v2, v1 being Element of L holds (v0 "\/" v2) "/\" ((v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" v2))) = v0 "\/" (v1 "/\" (v0 "\/" v2))

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "\/" v1) "/\" ((v0 "\/" v2) "/\" ((v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" v2)))) = (v0 "\/" v2) "/\" ((v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" v2))) by A162;
hence (v0 "\/" v2) "/\" ((v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" v2))) = v0 "\/" (v1 "/\" (v0 "\/" v2)) by A1082; :: thesis:

end;

A1089: for v2, v1, v0 being Element of L holds v0 "/\" (v1 "/\" (v1 "\/" (v2 "/\" (v0 "/\" v1)))) = v0 "/\" (v1 "/\" (v1 "\/" v2))

proof

let v2, v1, v0 be Element of L; :: thesis:
v1 "/\" (v1 "\/" ((v0 "/\" v1) "\/" v2)) = v1 "/\" (v1 "\/" (v2 "/\" (v0 "/\" v1))) by A1027;
hence v0 "/\" (v1 "/\" (v1 "\/" (v2 "/\" (v0 "/\" v1)))) = v0 "/\" (v1 "/\" (v1 "\/" v2)) by A414; :: thesis:

end;

A1091: for v1, v0, v2 being Element of L holds v0 "/\" (v1 "/\" (v1 "/\" (v1 "\/" (v2 "/\" v0)))) = v0 "/\" (v1 "/\" (v1 "\/" v2))

proof

let v1, v0, v2 be Element of L; :: thesis:
v1 "\/" (v2 "/\" (v0 "/\" v1)) = v1 "/\" (v1 "\/" (v2 "/\" v0)) by A441;
hence v0 "/\" (v1 "/\" (v1 "/\" (v1 "\/" (v2 "/\" v0)))) = v0 "/\" (v1 "/\" (v1 "\/" v2)) by A1089; :: thesis:

end;

A1093: for v1, v0, v2 being Element of L holds v0 "/\" (v1 "/\" (v1 "\/" (v2 "/\" v0))) = v0 "/\" (v1 "/\" (v1 "\/" v2))

proof

let v1, v0, v2 be Element of L; :: thesis:
v1 "/\" (v1 "/\" (v1 "\/" (v2 "/\" v0))) = v1 "/\" (v1 "\/" (v2 "/\" v0)) by A26;
hence v0 "/\" (v1 "/\" (v1 "\/" (v2 "/\" v0))) = v0 "/\" (v1 "/\" (v1 "\/" v2)) by A1091; :: thesis:

end;

A1095: for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" (v0 "/\" (v0 "\/" v1))) = v0 "/\" ((v0 "/\" v1) "\/" v2)

proof

let v2, v1, v0 be Element of L; :: thesis:
v2 "/\" (v0 "/\" (v0 "\/" (v1 "/\" v2))) = v2 "/\" (v0 "/\" (v0 "\/" v1)) by A1093;
hence (v0 "/\" v1) "\/" (v2 "/\" (v0 "/\" (v0 "\/" v1))) = v0 "/\" ((v0 "/\" v1) "\/" v2) by A919; :: thesis:

end;

A1097: for v2, v1, v0 being Element of L holds v0 "\/" (v0 "/\" ((v0 "/\" v1) "\/" v2)) = v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" v2))

proof

let v2, v1, v0 be Element of L; :: thesis:
(v0 "/\" v1) "\/" (v2 "/\" (v0 "/\" (v0 "\/" v1))) = v0 "/\" ((v0 "/\" v1) "\/" v2) by A1095;
hence v0 "\/" (v0 "/\" ((v0 "/\" v1) "\/" v2)) = v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" v2)) by A921; :: thesis:

end;

A1099: for v2, v1, v0 being Element of L holds v0 "/\" (v0 "\/" ((v0 "/\" v1) "\/" v2)) = v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" v2))

proof

let v2, v1, v0 be Element of L; :: thesis:
v0 "\/" (v0 "/\" ((v0 "/\" v1) "\/" v2)) = v0 "/\" (v0 "\/" ((v0 "/\" v1) "\/" v2)) by A347;
hence v0 "/\" (v0 "\/" ((v0 "/\" v1) "\/" v2)) = v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" v2)) by A1097; :: thesis:

end;

A1101: for v2, v1, v0 being Element of L holds v0 "/\" (v0 "\/" (v2 "/\" (v0 "/\" v1))) = v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" v2))

proof

let v2, v1, v0 be Element of L; :: thesis:
v0 "/\" (v0 "\/" ((v0 "/\" v1) "\/" v2)) = v0 "/\" (v0 "\/" (v2 "/\" (v0 "/\" v1))) by A1027;
hence v0 "/\" (v0 "\/" (v2 "/\" (v0 "/\" v1))) = v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" v2)) by A1099; :: thesis:

end;

A1104: for v0, v2, v1 being Element of L holds v0 "/\" (v0 "/\" (v0 "\/" (v1 "/\" v2))) = v0 "/\" ((v0 "\/" v2) "/\" (v0 "\/" v1))

proof

let v0, v2, v1 be Element of L; :: thesis:
v0 "\/" (v1 "/\" (v0 "/\" v2)) = v0 "/\" (v0 "\/" (v1 "/\" v2)) by A417;
hence v0 "/\" (v0 "/\" (v0 "\/" (v1 "/\" v2))) = v0 "/\" ((v0 "\/" v2) "/\" (v0 "\/" v1)) by A1101; :: thesis:

end;

A1106: for v0, v2, v1 being Element of L holds v0 "/\" (v0 "\/" (v1 "/\" v2)) = v0 "/\" ((v0 "\/" v2) "/\" (v0 "\/" v1))

proof

let v0, v2, v1 be Element of L; :: thesis:
v0 "/\" (v0 "/\" (v0 "\/" (v1 "/\" v2))) = v0 "/\" (v0 "\/" (v1 "/\" v2)) by A26;
hence v0 "/\" (v0 "\/" (v1 "/\" v2)) = v0 "/\" ((v0 "\/" v2) "/\" (v0 "\/" v1)) by A1104; :: thesis:

end;

A1108: for v0, v2, v1 being Element of L holds v0 "/\" (v0 "\/" (v1 "\/" v2)) = v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" v2))

proof

let v0, v2, v1 be Element of L; :: thesis:
v0 "/\" (v0 "\/" (v2 "/\" v1)) = v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" v2)) by A1106;
hence v0 "/\" (v0 "\/" (v1 "\/" v2)) = v0 "/\" ((v0 "\/" v1) "/\" (v0 "\/" v2)) by A1027; :: thesis:

end;

A1111: for v100, v0, v1 being Element of L holds (v100 "\/" (v1 "\/" v0)) "/\" ((v1 "\/" v0) "/\" v100) = (v0 "\/" v1) "/\" ((v1 "\/" v0) "/\" v100)

proof

let v100, v0, v1 be Element of L; :: thesis:
(v0 "\/" v1) "/\" ((v1 "\/" v0) "/\" v100) = (v1 "\/" v0) "/\" v100 by A392;
hence (v100 "\/" (v1 "\/" v0)) "/\" ((v1 "\/" v0) "/\" v100) = (v0 "\/" v1) "/\" ((v1 "\/" v0) "/\" v100) by A717; :: thesis:

end;

A1114: for v0, v2, v1 being Element of L holds ((v1 "\/" v2) "/\" v0) "/\" (v0 "\/" (v1 "\/" v2)) = (v2 "\/" v1) "/\" ((v1 "\/" v2) "/\" v0)

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "\/" (v1 "\/" v2)) "/\" ((v1 "\/" v2) "/\" v0) = ((v1 "\/" v2) "/\" v0) "/\" (v0 "\/" (v1 "\/" v2)) by A4;
hence ((v1 "\/" v2) "/\" v0) "/\" (v0 "\/" (v1 "\/" v2)) = (v2 "\/" v1) "/\" ((v1 "\/" v2) "/\" v0) by A1111; :: thesis:

end;

A1117: for v2, v1, v0 being Element of L holds (v0 "\/" v1) "/\" (v2 "/\" (v2 "\/" (v0 "\/" v1))) = (v1 "\/" v0) "/\" ((v0 "\/" v1) "/\" v2)

proof

let v2, v1, v0 be Element of L; :: thesis:
((v0 "\/" v1) "/\" v2) "/\" (v2 "\/" (v0 "\/" v1)) = (v0 "\/" v1) "/\" (v2 "/\" (v2 "\/" (v0 "\/" v1))) by A3;
hence (v0 "\/" v1) "/\" (v2 "/\" (v2 "\/" (v0 "\/" v1))) = (v1 "\/" v0) "/\" ((v0 "\/" v1) "/\" v2) by A1114; :: thesis:

end;

A1119: for v1, v0, v2 being Element of L holds (v0 "\/" v1) "/\" (v2 "/\" ((v2 "\/" v0) "/\" (v2 "\/" v1))) = (v1 "\/" v0) "/\" ((v0 "\/" v1) "/\" v2)

proof

let v1, v0, v2 be Element of L; :: thesis:
v2 "/\" (v2 "\/" (v0 "\/" v1)) = v2 "/\" ((v2 "\/" v0) "/\" (v2 "\/" v1)) by A1108;
hence (v0 "\/" v1) "/\" (v2 "/\" ((v2 "\/" v0) "/\" (v2 "\/" v1))) = (v1 "\/" v0) "/\" ((v0 "\/" v1) "/\" v2) by A1117; :: thesis:

end;

A1121: for v1, v0, v2 being Element of L holds (v0 "\/" v1) "/\" (v2 "/\" ((v2 "\/" v0) "/\" (v2 "\/" v1))) = (v0 "\/" v1) "/\" v2

proof

let v1, v0, v2 be Element of L; :: thesis:
(v1 "\/" v0) "/\" ((v0 "\/" v1) "/\" v2) = (v0 "\/" v1) "/\" v2 by A392;
hence (v0 "\/" v1) "/\" (v2 "/\" ((v2 "\/" v0) "/\" (v2 "\/" v1))) = (v0 "\/" v1) "/\" v2 by A1119; :: thesis:

end;

A1123: for v2, v0, v1 being Element of L holds (v0 "\/" v1) "/\" (v1 "\/" ((v1 "\/" v0) "/\" v2)) = v1 "\/" ((v0 "\/" v1) "/\" v2)

proof

let v2, v0, v1 be Element of L; :: thesis:
v0 "\/" v1 = v1 "\/" v0 by A8;
hence (v0 "\/" v1) "/\" (v1 "\/" ((v1 "\/" v0) "/\" v2)) = v1 "\/" ((v0 "\/" v1) "/\" v2) by A208; :: thesis:

end;

A1125: for v2, v0, v1 being Element of L holds (v0 "\/" v1) "/\" ((v1 "\/" v0) "/\" (v1 "\/" v2)) = v1 "\/" ((v0 "\/" v1) "/\" v2)

proof

let v2, v0, v1 be Element of L; :: thesis:
v1 "\/" ((v1 "\/" v0) "/\" v2) = (v1 "\/" v0) "/\" (v1 "\/" v2) by A913;
hence (v0 "\/" v1) "/\" ((v1 "\/" v0) "/\" (v1 "\/" v2)) = v1 "\/" ((v0 "\/" v1) "/\" v2) by A1123; :: thesis:

end;

A1127: for v2, v0, v1 being Element of L holds (v1 "\/" v0) "/\" (v1 "\/" v2) = v1 "\/" ((v0 "\/" v1) "/\" v2)

proof

let v2, v0, v1 be Element of L; :: thesis:
(v0 "\/" v1) "/\" ((v1 "\/" v0) "/\" (v1 "\/" v2)) = (v1 "\/" v0) "/\" (v1 "\/" v2) by A392;
hence (v1 "\/" v0) "/\" (v1 "\/" v2) = v1 "\/" ((v0 "\/" v1) "/\" v2) by A1125; :: thesis:

end;

A1132: for v1, v101, v100 being Element of L holds (v100 "\/" v101) "/\" (v101 "\/" (v1 "/\" (v100 "\/" v101))) = v101 "\/" ((v100 "\/" v101) "/\" (v1 "/\" (v1 "\/" (v100 "\/" v101))))

proof

let v1, v101, v100 be Element of L; :: thesis:
(v100 "\/" v101) "/\" (v1 "/\" (v1 "\/" (v100 "\/" v101))) = v1 "/\" (v100 "\/" v101) by A308;
hence (v100 "\/" v101) "/\" (v101 "\/" (v1 "/\" (v100 "\/" v101))) = v101 "\/" ((v100 "\/" v101) "/\" (v1 "/\" (v1 "\/" (v100 "\/" v101)))) by A208; :: thesis:

end;

A1135: for v2, v1, v0 being Element of L holds v1 "\/" (v2 "/\" (v0 "\/" v1)) = v1 "\/" ((v0 "\/" v1) "/\" (v2 "/\" (v2 "\/" (v0 "\/" v1))))

proof

let v2, v1, v0 be Element of L; :: thesis:
(v0 "\/" v1) "/\" (v1 "\/" (v2 "/\" (v0 "\/" v1))) = v1 "\/" (v2 "/\" (v0 "\/" v1)) by A565;
hence v1 "\/" (v2 "/\" (v0 "\/" v1)) = v1 "\/" ((v0 "\/" v1) "/\" (v2 "/\" (v2 "\/" (v0 "\/" v1)))) by A1132; :: thesis:

end;

A1138: for v1, v0, v2 being Element of L holds v0 "\/" (v1 "/\" (v2 "\/" v0)) = v0 "\/" ((v2 "\/" v0) "/\" (v1 "/\" ((v1 "\/" v2) "/\" (v1 "\/" v0))))

proof

let v1, v0, v2 be Element of L; :: thesis:
v1 "/\" (v1 "\/" (v2 "\/" v0)) = v1 "/\" ((v1 "\/" v2) "/\" (v1 "\/" v0)) by A1108;
hence v0 "\/" (v1 "/\" (v2 "\/" v0)) = v0 "\/" ((v2 "\/" v0) "/\" (v1 "/\" ((v1 "\/" v2) "/\" (v1 "\/" v0)))) by A1135; :: thesis:

end;

A1140: for v1, v0, v2 being Element of L holds v0 "\/" (v1 "/\" (v2 "\/" v0)) = v0 "\/" ((v2 "\/" v0) "/\" v1)

proof

let v1, v0, v2 be Element of L; :: thesis:
(v2 "\/" v0) "/\" (v1 "/\" ((v1 "\/" v2) "/\" (v1 "\/" v0))) = (v2 "\/" v0) "/\" v1 by A1121;
hence v0 "\/" (v1 "/\" (v2 "\/" v0)) = v0 "\/" ((v2 "\/" v0) "/\" v1) by A1138; :: thesis:

end;

A1142: for v1, v0, v2 being Element of L holds v0 "\/" (v1 "/\" (v2 "\/" v0)) = (v0 "\/" v2) "/\" (v0 "\/" v1)

proof

let v1, v0, v2 be Element of L; :: thesis:
v0 "\/" ((v2 "\/" v0) "/\" v1) = (v0 "\/" v2) "/\" (v0 "\/" v1) by A1127;
hence v0 "\/" (v1 "/\" (v2 "\/" v0)) = (v0 "\/" v2) "/\" (v0 "\/" v1) by A1140; :: thesis:

end;

A1144: for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" (v0 "\/" v2)) "/\" (v0 "\/" (v2 "\/" v1)) = v0 "\/" (v2 "/\" v1)

proof

let v2, v1, v0 be Element of L; :: thesis:
v0 "\/" ((v1 "\/" v0) "/\" v2) = (v0 "\/" v1) "/\" (v0 "\/" v2) by A1127;
hence ((v0 "\/" v1) "/\" (v0 "\/" v2)) "/\" (v0 "\/" (v2 "\/" v1)) = v0 "\/" (v2 "/\" v1) by A1035; :: thesis:

end;

A1146: for v0, v1, v2 being Element of L holds (v0 "\/" v1) "/\" ((v0 "\/" v2) "/\" (v0 "\/" (v2 "\/" v1))) = v0 "\/" (v2 "/\" v1)

proof

let v0, v1, v2 be Element of L; :: thesis:
((v0 "\/" v1) "/\" (v0 "\/" v2)) "/\" (v0 "\/" (v2 "\/" v1)) = (v0 "\/" v1) "/\" ((v0 "\/" v2) "/\" (v0 "\/" (v2 "\/" v1))) by A3;
hence (v0 "\/" v1) "/\" ((v0 "\/" v2) "/\" (v0 "\/" (v2 "\/" v1))) = v0 "\/" (v2 "/\" v1) by A1144; :: thesis:

end;

A1148: for v1, v2, v0 being Element of L holds (v0 "\/" v2) "/\" (v0 "\/" v1) = (v0 "\/" v2) "/\" ((v0 "\/" v1) "/\" (v1 "\/" (v0 "\/" v2)))

proof

let v1, v2, v0 be Element of L; :: thesis:
v0 "\/" (v1 "/\" (v2 "\/" v0)) = (v0 "\/" v2) "/\" (v0 "\/" v1) by A1142;
hence (v0 "\/" v2) "/\" (v0 "\/" v1) = (v0 "\/" v2) "/\" ((v0 "\/" v1) "/\" (v1 "\/" (v0 "\/" v2))) by A1057; :: thesis:

end;

A1152: for v1, v2, v0 being Element of L holds v0 "\/" (v1 "/\" (v0 "\/" v2)) = v0 "\/" (v1 "/\" v2)

proof

let v1, v2, v0 be Element of L; :: thesis:
(v0 "\/" v2) "/\" ((v0 "\/" v1) "/\" (v0 "\/" (v1 "\/" v2))) = v0 "\/" (v1 "/\" v2) by A1146;
hence v0 "\/" (v1 "/\" (v0 "\/" v2)) = v0 "\/" (v1 "/\" v2) by A1084; :: thesis:

end;

A1154: for v0, v2, v1 being Element of L holds v0 "\/" (v1 "/\" v2) = (v0 "\/" v2) "/\" ((v0 "\/" v1) "/\" (v1 "\/" (v0 "\/" v2)))

proof

let v0, v2, v1 be Element of L; :: thesis:
v0 "\/" (v1 "/\" (v0 "\/" v2)) = v0 "\/" (v1 "/\" v2) by A1152;
hence v0 "\/" (v1 "/\" v2) = (v0 "\/" v2) "/\" ((v0 "\/" v1) "/\" (v1 "\/" (v0 "\/" v2))) by A969; :: thesis:

end;

Z: for v0, v2, v1 being Element of L holds v0 "\/" (v1 "/\" v2) = (v0 "\/" v2) "/\" (v0 "\/" v1)

proof

let v0, v2, v1 be Element of L; :: thesis:
(v0 "\/" v2) "/\" ((v0 "\/" v1) "/\" (v1 "\/" (v0 "\/" v2))) = (v0 "\/" v2) "/\" (v0 "\/" v1) by A1148;
hence v0 "\/" (v1 "/\" v2) = (v0 "\/" v2) "/\" (v0 "\/" v1) by A1154; :: thesis:

end;

let v1, v2, v3 be Element of L; :: thesis:
v1 "\/" (v2 "/\" v3) = (v1 "\/" v3) "/\" (v1 "\/" v2) by Z;
hence v1 "\/" (v2 "/\" v3) = (v1 "\/" v2) "/\" (v1 "\/" v3) by A4; :: thesis: