proof

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

end;

assume A11: for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" (v0 "\/" v1)) = (v0 "\/" v1) "/\" (v2 "\/" (v0 "/\" v1)) ; :: thesis:
A14: 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 A7;
hence (v0 "/\" v1) "\/" (v0 "/\" (v1 "\/" v2)) = v0 "/\" (v1 "\/" v2) by A4; :: thesis:

end;

A17: 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 A1;
hence v101 "/\" v102 = v101 "/\" (v101 "/\" v102) by A2; :: thesis:

end;

A22: 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 A1;
hence (v100 "/\" v102) "/\" v102 = v100 "/\" v102 by A2; :: thesis:

end;

A25: 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 A3;
hence v1 "/\" (v0 "/\" v1) = v0 "/\" v1 by A22; :: thesis:

end;

A28: 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 A3;
hence (v1 "/\" v0) "/\" v2 = v0 "/\" (v1 "/\" v2) by A2; :: thesis:

end;

A31: 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 A2;
hence v0 "/\" (v1 "/\" v2) = v1 "/\" (v0 "/\" v2) by A28; :: thesis:

end;

A34: 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 A5;
hence v101 "\/" v102 = v101 "\/" (v101 "\/" v102) by A6; :: thesis:

end;

A39: 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 A5;
hence (v100 "\/" v102) "\/" v102 = v100 "\/" v102 by A6; :: thesis:

end;

A42: 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 A7;
hence v1 "\/" (v0 "\/" v1) = v0 "\/" v1 by A39; :: thesis:

end;

A45: 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 A7;
hence (v1 "\/" v0) "\/" v2 = v0 "\/" (v1 "\/" v2) by A6; :: thesis:

end;

A48: 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 A6;
hence v0 "\/" (v1 "\/" v2) = v1 "\/" (v0 "\/" v2) by A45; :: thesis:

end;

A51: 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 A10;
hence (v0 "\/" (v1 "/\" v2)) "/\" v102 = (v0 "\/" v1) "/\" ((v0 "\/" (v1 "/\" v2)) "/\" v102) by A2; :: thesis:

end;

A55: 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 A7;
hence (v1 "\/" v0) "/\" (v0 "\/" (v1 "/\" v2)) = v0 "\/" (v1 "/\" v2) by A10; :: thesis:

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

A74: 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 A3;
hence (v1 "/\" v0) "\/" (v0 "/\" (v1 "\/" v2)) = v0 "/\" (v1 "\/" v2) by A14; :: thesis:

end;

A77: 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 A7;
hence (v0 "/\" v1) "\/" (v0 "/\" (v2 "\/" v1)) = v0 "/\" (v1 "\/" v2) by A14; :: thesis:

end;

A80: 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 A14;
hence ((v101 "/\" v1) "\/" v101) "/\" (v101 "/\" (v1 "\/" v2)) = (v101 "/\" v1) "\/" (v101 "/\" (v1 "\/" v2)) by A10; :: thesis:

end;

A83: 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 A7;
hence (v0 "\/" (v0 "/\" v1)) "/\" (v0 "/\" (v1 "\/" v2)) = (v0 "/\" v1) "\/" (v0 "/\" (v1 "\/" v2)) by A80; :: thesis:

end;

A85: 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 A31;
hence v0 "/\" ((v0 "\/" (v0 "/\" v1)) "/\" (v1 "\/" v2)) = (v0 "/\" v1) "\/" (v0 "/\" (v1 "\/" v2)) by A83; :: thesis:

end;

A87: 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 A14;
hence v0 "/\" ((v0 "\/" (v0 "/\" v1)) "/\" (v1 "\/" v2)) = v0 "/\" (v1 "\/" v2) by A85; :: thesis:

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

A100: 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 A17;
hence (v100 "/\" v1) "\/" (v100 "/\" ((v100 "/\" v1) "\/" v102)) = v100 "/\" ((v100 "/\" v1) "\/" v102) by A14; :: thesis:

end;

A104: 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 A6;
hence v100 "\/" (v0 "\/" (v1 "\/" v100)) = (v0 "\/" v1) "\/" v100 by A42; :: thesis:

end;

A107: 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 A6;
hence v0 "\/" (v1 "\/" (v2 "\/" v0)) = v1 "\/" (v2 "\/" v0) by A104; :: thesis:

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

A117: 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 by A7;
hence v0 "\/" (v0 "/\" v1) = v0 "/\" (v0 "\/" v1) by A109; :: thesis:

end;

A119: 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 "\/" (v0 "/\" v1) = v0 "/\" (v0 "\/" v1) by A117;
hence v0 "/\" ((v0 "/\" (v0 "\/" v1)) "/\" (v1 "\/" v2)) = v0 "/\" (v1 "\/" v2) by A87; :: thesis:

end;

A121: 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 "/\" (v0 "\/" v1)) "/\" (v1 "\/" v2) = v0 "/\" ((v0 "\/" v1) "/\" (v1 "\/" v2)) by A2;
hence v0 "/\" (v0 "/\" ((v0 "\/" v1) "/\" (v1 "\/" v2))) = v0 "/\" (v1 "\/" v2) by A119; :: thesis:

end;

A123: 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 A17;
hence v0 "/\" ((v0 "\/" v1) "/\" (v1 "\/" v2)) = v0 "/\" (v1 "\/" v2) by A121; :: thesis:

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

A148: 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 A133;
hence (v100 "\/" v101) "/\" ((v101 "/\" v102) "\/" v100) = (v100 "\/" (v101 "/\" v102)) "/\" ((v101 "/\" v102) "\/" v100) by A51; :: thesis:

end;

A151: 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 A133;
hence (v0 "\/" v1) "/\" ((v1 "/\" v2) "\/" v0) = (v1 "/\" v2) "\/" v0 by A148; :: thesis:

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

A168: 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 A10;
hence ((v101 "\/" v1) "/\" v101) "\/" ((v101 "\/" v1) "/\" ((v1 "/\" v2) "\/" v101)) = v101 "\/" (v1 "/\" v2) by A77; :: thesis:

end;

A171: 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 A3;
hence (v0 "/\" (v0 "\/" v1)) "\/" ((v0 "\/" v1) "/\" ((v1 "/\" v2) "\/" v0)) = v0 "\/" (v1 "/\" v2) by A168; :: thesis:

end;

A173: 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 A151;
hence (v0 "/\" (v0 "\/" v1)) "\/" ((v1 "/\" v2) "\/" v0) = v0 "\/" (v1 "/\" v2) by A171; :: thesis:

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

A183: 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 A117;
hence v100 "/\" ((v100 "/\" (v100 "\/" v1)) "/\" ((v100 "/\" v1) "\/" v102)) = v100 "/\" ((v100 "/\" v1) "\/" v102) by A123; :: thesis:

end;

A186: 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 A2;
hence v0 "/\" (v0 "/\" ((v0 "\/" v1) "/\" ((v0 "/\" v1) "\/" v2))) = v0 "/\" ((v0 "/\" v1) "\/" v2) by A183; :: thesis:

end;

A188: 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 A17;
hence v0 "/\" ((v0 "\/" v1) "/\" ((v0 "/\" v1) "\/" v2)) = v0 "/\" ((v0 "/\" v1) "\/" v2) by A186; :: thesis:

end;

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

proof

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

end;

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

proof

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

end;

A196: for v2, v1, v0 being Element of L holds (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) by A117;
hence (v0 "/\" v1) "\/" (v2 "/\" (v0 "/\" (v0 "\/" v1))) = (v0 "\/" (v0 "/\" v1)) "/\" ((v0 "/\" (v0 "/\" v1)) "\/" v2) by A193; :: thesis:

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

A204: for v2, v1, v0 being Element of L holds (v0 "\/" v1) "/\" ((v0 "/\" v1) "\/" (v2 "/\" v0)) = v0 "/\" ((v0 "\/" v1) "/\" ((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 A2;
hence (v0 "\/" v1) "/\" ((v0 "/\" v1) "\/" (v2 "/\" v0)) = v0 "/\" ((v0 "\/" v1) "/\" ((v0 "/\" v1) "\/" v2)) by A202; :: thesis:

end;

A206: for v2, v1, v0 being Element of L holds (v0 "\/" v1) "/\" ((v0 "/\" v1) "\/" (v2 "/\" v0)) = 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 A188;
hence (v0 "\/" v1) "/\" ((v0 "/\" v1) "\/" (v2 "/\" v0)) = v0 "/\" ((v0 "/\" v1) "\/" v2) by A204; :: thesis:

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

hence for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) ; :: thesis: