let L be non empty LattStr ; :: thesis:
assume A2: for v0 being Element of L holds v0 "/\" v0 = v0 ; :: thesis:
assume A3: for v1, v0 being Element of L holds v0 "/\" v1 = v1 "/\" v0 ; :: thesis:
assume A4: for v0 being Element of L holds v0 "\/" v0 = v0 ; :: thesis:
assume A5: for v1, v0 being Element of L holds v0 "\/" v1 = v1 "\/" v0 ; :: thesis:
assume A6: for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" (v2 "\/" v1)) "/\" v1 = v1 ; :: thesis:
A8: for v2, v1, v0 being Element of L holds v1 "/\" ((v0 "\/" v1) "/\" (v2 "\/" v1)) = v1

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

end;

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

proof

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

end;

A79: 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 "/\" v1) "\/" (v0 "/\" v1) = v0 "/\" v1 by A4;
hence (v0 "/\" v1) "/\" (v1 "/\" v0) = (v0 "/\" v1) "\/" (v0 "/\" v1) by A76; :: thesis:

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

let v101, v3, v100 be Element of L; :: thesis:
v100 "\/" ((v100 "/\" v101) "\/" (v101 "/\" (v100 "/\" v3))) = v100 by A123;
hence ((v100 "/\" v101) "\/" (v101 "/\" (v100 "/\" v3))) "/\" (v101 "/\" v100) = (v100 "/\" v101) "\/" (v101 "/\" (v100 "/\" v3)) by A61; :: thesis:

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

end;

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

proof

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

end;

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

end;

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