let L be non empty LattStr ; :: thesis: ( ( for v0 being Element of L holds v0 "/\" v0 = v0 ) & ( for v2, v1, v0 being Element of L holds (v0 "/\" v1) "/\" v2 = v0 "/\" (v1 "/\" v2) ) & ( for v1, v0 being Element of L holds v0 "/\" v1 = v1 "/\" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) ) & ( for v0 being Element of L holds v0 "\/" v0 = v0 ) & ( for v2, v1, v0 being Element of L holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) ) & ( for v1, v0 being Element of L holds v0 "\/" v1 = v1 "\/" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) ) & ( for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" (v0 "\/" v1)) = (v0 "\/" v1) "/\" (v2 "\/" (v0 "/\" v1)) ) implies for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) )
assume A1: for v0 being Element of L holds v0 "/\" v0 = v0 ; :: thesis: ( ex v2, v1, v0 being Element of L st not (v0 "/\" v1) "/\" v2 = v0 "/\" (v1 "/\" v2) or ex v1, v0 being Element of L st not v0 "/\" v1 = v1 "/\" v0 or ex v0, v2, v1 being Element of L st not (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) or ex v0 being Element of L st not v0 "\/" v0 = v0 or ex v2, v1, v0 being Element of L st not (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) or ex v1, v0 being Element of L st not v0 "\/" v1 = v1 "\/" v0 or ex v0, v2, v1 being Element of L st not (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) or ex v2, v1, v0 being Element of L st not (v0 "/\" v1) "\/" (v2 "/\" (v0 "\/" v1)) = (v0 "\/" v1) "/\" (v2 "\/" (v0 "/\" v1)) or for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) )
assume A2: for v2, v1, v0 being Element of L holds (v0 "/\" v1) "/\" v2 = v0 "/\" (v1 "/\" v2) ; :: thesis: ( ex v1, v0 being Element of L st not v0 "/\" v1 = v1 "/\" v0 or ex v0, v2, v1 being Element of L st not (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) or ex v0 being Element of L st not v0 "\/" v0 = v0 or ex v2, v1, v0 being Element of L st not (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) or ex v1, v0 being Element of L st not v0 "\/" v1 = v1 "\/" v0 or ex v0, v2, v1 being Element of L st not (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) or ex v2, v1, v0 being Element of L st not (v0 "/\" v1) "\/" (v2 "/\" (v0 "\/" v1)) = (v0 "\/" v1) "/\" (v2 "\/" (v0 "/\" v1)) or for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) )
assume A3: for v1, v0 being Element of L holds v0 "/\" v1 = v1 "/\" v0 ; :: thesis: ( ex v0, v2, v1 being Element of L st not (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) or ex v0 being Element of L st not v0 "\/" v0 = v0 or ex v2, v1, v0 being Element of L st not (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) or ex v1, v0 being Element of L st not v0 "\/" v1 = v1 "\/" v0 or ex v0, v2, v1 being Element of L st not (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) or ex v2, v1, v0 being Element of L st not (v0 "/\" v1) "\/" (v2 "/\" (v0 "\/" v1)) = (v0 "\/" v1) "/\" (v2 "\/" (v0 "/\" v1)) or for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) )
assume A4: for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) ; :: thesis: ( ex v0 being Element of L st not v0 "\/" v0 = v0 or ex v2, v1, v0 being Element of L st not (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) or ex v1, v0 being Element of L st not v0 "\/" v1 = v1 "\/" v0 or ex v0, v2, v1 being Element of L st not (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) or ex v2, v1, v0 being Element of L st not (v0 "/\" v1) "\/" (v2 "/\" (v0 "\/" v1)) = (v0 "\/" v1) "/\" (v2 "\/" (v0 "/\" v1)) or for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) )
assume A5: for v0 being Element of L holds v0 "\/" v0 = v0 ; :: thesis: ( ex v2, v1, v0 being Element of L st not (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) or ex v1, v0 being Element of L st not v0 "\/" v1 = v1 "\/" v0 or ex v0, v2, v1 being Element of L st not (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) or ex v2, v1, v0 being Element of L st not (v0 "/\" v1) "\/" (v2 "/\" (v0 "\/" v1)) = (v0 "\/" v1) "/\" (v2 "\/" (v0 "/\" v1)) or for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) )
assume A6: for v2, v1, v0 being Element of L holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) ; :: thesis: ( ex v1, v0 being Element of L st not v0 "\/" v1 = v1 "\/" v0 or ex v0, v2, v1 being Element of L st not (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) or ex v2, v1, v0 being Element of L st not (v0 "/\" v1) "\/" (v2 "/\" (v0 "\/" v1)) = (v0 "\/" v1) "/\" (v2 "\/" (v0 "/\" v1)) or for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) )
assume A7: for v1, v0 being Element of L holds v0 "\/" v1 = v1 "\/" v0 ; :: thesis: ( ex v0, v2, v1 being Element of L st not (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) or ex v2, v1, v0 being Element of L st not (v0 "/\" v1) "\/" (v2 "/\" (v0 "\/" v1)) = (v0 "\/" v1) "/\" (v2 "\/" (v0 "/\" v1)) or for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) )
assume A8: for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) ; :: thesis: ( ex v2, v1, v0 being Element of L st not (v0 "/\" v1) "\/" (v2 "/\" (v0 "\/" v1)) = (v0 "\/" v1) "/\" (v2 "\/" (v0 "/\" v1)) or for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) )
A10: 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) "/\" (v0 "\/" (v1 "/\" v2)) = v0 "\/" (v1 "/\" v2)
(v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = (v0 "\/" v1) "/\" (v0 "\/" (v1 "/\" v2)) by A3;
hence (v0 "\/" v1) "/\" (v0 "\/" (v1 "/\" v2)) = v0 "\/" (v1 "/\" v2) by A8; :: thesis: verum

end;

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

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

end;

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

proof

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

end;

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

proof

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

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

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

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

end;

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

proof

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

end;

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

proof

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

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

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

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

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

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

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 "\/" (v1 "/\" v0) = (v0 "\/" v0) "/\" (v1 "\/" (v0 "/\" v0))
v0 "\/" v0 = v0 by A5;
hence v0 "\/" (v1 "/\" v0) = (v0 "\/" v0) "/\" (v1 "\/" (v0 "/\" v0)) by A59; :: thesis: verum

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 "\/" (v1 "/\" v0) = v0 "/\" (v1 "\/" (v0 "/\" v0))
v0 "\/" v0 = v0 by A5;
hence v0 "\/" (v1 "/\" v0) = v0 "/\" (v1 "\/" (v0 "/\" v0)) by A62; :: thesis: verum

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 "\/" (v1 "/\" v0) = v0 "/\" (v1 "\/" v0)
v0 "/\" v0 = v0 by A1;
hence v0 "\/" (v1 "/\" v0) = v0 "/\" (v1 "\/" v0) by A64; :: thesis: verum

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: (v100 "/\" v101) "\/" (v0 "/\" (v1 "/\" (v100 "\/" v101))) = (v100 "\/" v101) "/\" ((v0 "/\" v1) "\/" (v100 "/\" v101))
(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: verum

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

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

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

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) "/\" (v101 "/\" (v1 "\/" v2)) = (v101 "/\" v1) "\/" (v101 "/\" (v1 "\/" v2))
(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: verum

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

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 "\/" (v0 "/\" v1)) "/\" (v1 "\/" v2)) = (v0 "/\" v1) "\/" (v0 "/\" (v1 "\/" v2))
(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: verum

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

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 "/\" v2)) "\/" ((v0 "\/" v1) "/\" ((v0 "\/" (v1 "/\" v2)) "\/" v102)) = (v0 "\/" v1) "/\" ((v0 "\/" (v1 "/\" v2)) "\/" v102)
(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: verum

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)) "\/" ((v0 "\/" v1) "/\" (v0 "\/" ((v1 "/\" v2) "\/" v3))) = (v0 "\/" v1) "/\" ((v0 "\/" (v1 "/\" v2)) "\/" v3)
(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: verum

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) "/\" ((v0 "\/" (v1 "/\" v2)) "\/" v3)
(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: verum

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) "\/" ((v0 "\/" v1) "/\" (v0 "\/" ((v1 "/\" v2) "\/" v3)))) = (v0 "\/" v1) "/\" (v0 "\/" ((v1 "/\" v2) "\/" v3))
(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: verum

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

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

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

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

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

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

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

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

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 "/\" ((v0 "\/" v1) "/\" (v1 "\/" v2))) = v0 "/\" (v1 "\/" v2)
(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: verum

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 "\/" v1) "/\" (v1 "\/" v2)) = v0 "/\" (v1 "\/" v2)
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: verum

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

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

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 "\/" v1) "/\" (v1 "\/" v0) = v1 "\/" v0
v0 "/\" v0 = v0 by A1;
hence (v0 "\/" v1) "/\" (v1 "\/" v0) = v1 "\/" v0 by A130; :: thesis: verum

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 "\/" v101) "/\" (v101 "\/" (v1 "/\" v100)) = v101 "\/" (v100 "/\" (v1 "/\" v100))
v100 "/\" (v1 "/\" v100) = v1 "/\" v100 by A25;
hence (v100 "\/" v101) "/\" (v101 "\/" (v1 "/\" v100)) = v101 "\/" (v100 "/\" (v1 "/\" v100)) by A55; :: thesis: verum

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

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

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 "/\" v1) "\/" (v0 "/\" v2)
(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: verum

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) "/\" ((v101 "/\" v102) "\/" v100) = (v100 "\/" (v101 "/\" v102)) "/\" ((v101 "/\" v102) "\/" v100)
(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: verum

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

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

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 "/\" v1) "\/" (v1 "/\" v0) = v1 "/\" v0
v0 "\/" v0 = v0 by A5;
hence (v0 "/\" v1) "\/" (v1 "/\" v0) = v1 "/\" v0 by A154; :: thesis: verum

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

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: (v1 "/\" v0) "\/" v102 = (v0 "/\" v1) "\/" ((v1 "/\" v0) "\/" v102)
(v0 "/\" v1) "\/" (v1 "/\" v0) = v1 "/\" v0 by A157;
hence (v1 "/\" v0) "\/" v102 = (v0 "/\" v1) "\/" ((v1 "/\" v0) "\/" v102) by A6; :: thesis: verum

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) "\/" ((v101 "\/" v1) "/\" ((v1 "/\" v2) "\/" v101)) = v101 "\/" (v1 "/\" v2)
(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: verum

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

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

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 "\/" ((v1 "/\" v0) "\/" ((v1 "/\" v2) "\/" v0)) = v0 "\/" (v1 "/\" v2)
(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: verum

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: (v1 "/\" v0) "\/" ((v1 "/\" v2) "\/" v0) = v0 "\/" (v1 "/\" v2)
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: verum

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: (v0 "/\" v1) "\/" (v2 "/\" (v3 "/\" (v0 "\/" v1))) = (v0 "\/" v1) "/\" ((v0 "/\" v1) "\/" (v2 "/\" v3))
(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: verum

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

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 "/\" ((v0 "\/" v1) "/\" ((v0 "/\" v1) "\/" v2))) = v0 "/\" ((v0 "/\" v1) "\/" v2)
(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: verum

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 "\/" v1) "/\" ((v0 "/\" v1) "\/" v2)) = v0 "/\" ((v0 "/\" v1) "\/" v2)
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: verum

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 "/\" v2)) = (v0 "/\" v1) "\/" (v0 "/\" v2)
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: verum

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

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 "/\" v1) "\/" (v2 "/\" (v0 "/\" (v0 "\/" v1))) = (v0 "\/" (v0 "/\" v1)) "/\" ((v0 "/\" (v0 "/\" v1)) "\/" v2)
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: verum

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) "/\" ((v0 "/\" v1) "\/" (v2 "/\" v0)) = (v0 "\/" (v0 "/\" v1)) "/\" ((v0 "/\" (v0 "/\" v1)) "\/" v2)
(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: verum

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 "\/" v1) "/\" ((v0 "/\" v1) "\/" (v2 "/\" v0)) = (v0 "/\" (v0 "\/" v1)) "/\" ((v0 "/\" (v0 "/\" v1)) "\/" v2)
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: verum

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

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 "\/" v1) "/\" ((v0 "/\" v1) "\/" (v2 "/\" v0)) = v0 "/\" ((v0 "\/" v1) "/\" ((v0 "/\" v1) "\/" v2))
(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: verum

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 "\/" v1) "/\" ((v0 "/\" v1) "\/" (v2 "/\" v0)) = v0 "/\" ((v0 "/\" v1) "\/" v2)
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: verum

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

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 "/\" v1) "\/" (v2 "/\" v0)
(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: verum

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 "/\" (v0 "/\" ((v0 "/\" v1) "\/" v2)) = (v0 "/\" v1) "\/" (v2 "/\" v0)
(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: verum

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

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: (v100 "/\" (v0 "\/" v100)) "\/" (v100 "\/" (v2 "/\" v0)) = (v0 "\/" v100) "/\" (v100 "\/" (v2 "/\" v0))
(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: verum

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 "\/" ((v0 "/\" (v1 "\/" v0)) "\/" (v2 "/\" v1)) = (v1 "\/" v0) "/\" (v0 "\/" (v2 "/\" v1))
(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: verum

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 "\/" (v0 "\/" ((v1 "/\" v0) "\/" (v2 "/\" v1))) = (v1 "\/" v0) "/\" (v0 "\/" (v2 "/\" v1))
(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: verum

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: v0 "\/" (v0 "\/" (v1 "/\" ((v1 "/\" v0) "\/" v2))) = (v1 "\/" v0) "/\" (v0 "\/" (v2 "/\" v1))
(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: verum

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 "\/" (v1 "/\" ((v1 "/\" v0) "\/" v2)) = (v1 "\/" v0) "/\" (v0 "\/" (v2 "/\" v1))
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: verum

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: v0 "\/" (v1 "/\" ((v1 "/\" v0) "\/" v2)) = v0 "\/" (v2 "/\" v1)
(v1 "\/" v0) "/\" (v0 "\/" (v2 "/\" v1)) = v0 "\/" (v2 "/\" v1) by A139;
hence v0 "\/" (v1 "/\" ((v1 "/\" v0) "\/" v2)) = v0 "\/" (v2 "/\" v1) by A229; :: thesis: verum

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: (v1 "/\" v100) "\/" ((v100 "/\" v102) "\/" (v1 "/\" v100)) = (v1 "/\" v100) "\/" (v100 "/\" v102)
v100 "/\" (v1 "/\" v100) = v1 "/\" v100 by A25;
hence (v1 "/\" v100) "\/" ((v100 "/\" v102) "\/" (v1 "/\" v100)) = (v1 "/\" v100) "\/" (v100 "/\" v102) by A177; :: thesis: verum

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: (v0 "/\" v1) "\/" (v1 "/\" ((v1 "/\" v2) "\/" v0)) = (v0 "/\" v1) "\/" (v1 "/\" v2)
(v1 "/\" v2) "\/" (v0 "/\" v1) = v1 "/\" ((v1 "/\" v2) "\/" v0) by A216;
hence (v0 "/\" v1) "\/" (v1 "/\" ((v1 "/\" v2) "\/" v0)) = (v0 "/\" v1) "\/" (v1 "/\" v2) by A234; :: thesis: verum

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: v1 "/\" (v0 "\/" (v1 "/\" v2)) = (v0 "/\" v1) "\/" (v1 "/\" v2)
(v0 "/\" v1) "\/" (v1 "/\" ((v1 "/\" v2) "\/" v0)) = v1 "/\" (v0 "\/" (v1 "/\" v2)) by A159;
hence v1 "/\" (v0 "\/" (v1 "/\" v2)) = (v0 "/\" v1) "\/" (v1 "/\" v2) by A237; :: thesis: verum

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) "\/" (((v102 "/\" v101) "\/" v101) "/\" ((v101 "/\" v102) "\/" v103))) = ((v102 "/\" v101) "\/" v101) "/\" ((v102 "/\" v101) "\/" ((v101 "/\" v102) "\/" v103))
(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: verum

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 "/\" v0) "\/" ((v1 "\/" (v0 "/\" v1)) "/\" ((v1 "/\" v0) "\/" v2))) = ((v0 "/\" v1) "\/" v1) "/\" ((v0 "/\" v1) "\/" ((v1 "/\" v0) "\/" v2))
(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: verum

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: (v0 "/\" v1) "\/" ((v1 "/\" v0) "\/" ((v1 "/\" (v1 "\/" v0)) "/\" ((v1 "/\" v0) "\/" v2))) = ((v0 "/\" v1) "\/" v1) "/\" ((v0 "/\" v1) "\/" ((v1 "/\" v0) "\/" v2))
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: verum

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: (v0 "/\" v1) "\/" ((v1 "/\" v0) "\/" (v1 "/\" ((v1 "\/" v0) "/\" ((v1 "/\" v0) "\/" v2)))) = ((v0 "/\" v1) "\/" v1) "/\" ((v0 "/\" v1) "\/" ((v1 "/\" v0) "\/" v2))
(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: verum

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: (v0 "/\" v1) "\/" ((v1 "/\" v0) "\/" (v1 "/\" ((v1 "/\" v0) "\/" v2))) = ((v0 "/\" v1) "\/" v1) "/\" ((v0 "/\" v1) "\/" ((v1 "/\" v0) "\/" v2))
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: verum

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: (v0 "/\" v1) "\/" (v1 "/\" ((v1 "/\" v0) "\/" v2)) = ((v0 "/\" v1) "\/" v1) "/\" ((v0 "/\" v1) "\/" ((v1 "/\" v0) "\/" v2))
(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: verum

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: v1 "/\" (v0 "\/" (v1 "/\" ((v1 "/\" v0) "\/" v2))) = ((v0 "/\" v1) "\/" v1) "/\" ((v0 "/\" v1) "\/" ((v1 "/\" v0) "\/" v2))
(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: verum

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: v0 "/\" (v1 "\/" (v2 "/\" v0)) = ((v1 "/\" v0) "\/" v0) "/\" ((v1 "/\" v0) "\/" ((v0 "/\" v1) "\/" v2))
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: verum

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

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 "\/" (v2 "/\" v0)) = (v0 "/\" (v0 "\/" v1)) "/\" ((v1 "/\" v0) "\/" ((v0 "/\" v1) "\/" v2))
v0 "\/" (v1 "/\" v0) = v0 "/\" (v0 "\/" v1) by A115;
hence v0 "/\" (v1 "\/" (v2 "/\" v0)) = (v0 "/\" (v0 "\/" v1)) "/\" ((v1 "/\" v0) "\/" ((v0 "/\" v1) "\/" v2)) by A263; :: thesis: verum

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: v0 "/\" (v1 "\/" (v2 "/\" v0)) = (v0 "/\" (v0 "\/" v1)) "/\" ((v0 "/\" v1) "\/" v2)
(v1 "/\" v0) "\/" ((v0 "/\" v1) "\/" v2) = (v0 "/\" v1) "\/" v2 by A162;
hence v0 "/\" (v1 "\/" (v2 "/\" v0)) = (v0 "/\" (v0 "\/" v1)) "/\" ((v0 "/\" v1) "\/" v2) by A265; :: thesis: verum

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 "/\" (v1 "\/" (v2 "/\" v0)) = v0 "/\" ((v0 "\/" v1) "/\" ((v0 "/\" v1) "\/" v2))
(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: verum

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

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 "/\" (v1 "\/" ((v0 "/\" v2) "/\" v0)) = (v0 "/\" v1) "\/" (v0 "/\" v2)
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: verum

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

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

end;

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