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

end;

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

proof

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

end;

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

end;

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

end;

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

end;

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

end;

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

end;

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

proof

let v102, v101 be Element of L; :: thesis: v101 "/\" (v101 "\/" (v101 "/\" v102)) = v101 "\/" (v101 "/\" v102)
v101 "\/" v101 = v101 by A4;
hence v101 "/\" (v101 "\/" (v101 "/\" v102)) = v101 "\/" (v101 "/\" v102) by A9; :: thesis: verum

end;

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

proof

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

end;

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

proof

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

end;

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

end;

A44: 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 A9;
hence ((v101 "\/" v1) "/\" v101) "\/" (v101 "\/" (v1 "/\" v2)) = (v101 "\/" v1) "/\" (v101 "\/" (v1 "/\" v2)) by A16; :: thesis: verum

end;

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

end;

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

end;

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

end;

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

proof

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

end;

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

proof

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

end;

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

end;

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

end;

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

end;

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

proof

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

end;

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

proof

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

end;

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

end;

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

proof

let v100, v2 be Element of L; :: thesis: v100 "/\" (v100 "\/" (v2 "/\" v100)) = v100 "\/" (v100 "/\" (v100 "\/" v2))
v100 "\/" (v100 "/\" (v100 "\/" v2)) = v100 "\/" (v2 "/\" v100) by A68;
hence v100 "/\" (v100 "\/" (v2 "/\" v100)) = v100 "\/" (v100 "/\" (v100 "\/" v2)) by A31; :: thesis: verum

end;

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

proof

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

end;

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

end;

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

end;

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

end;

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

end;

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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