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 v0, v1, v2 being Element of L st v0 "\/" v1 = v1 holds
v0 "\/" (v2 "/\" v1) = (v0 "\/" v2) "/\" v1 ) implies for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) )
assume A2: 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 v0, v1, v2 being Element of L st
( v0 "\/" v1 = v1 & not v0 "\/" (v2 "/\" v1) = (v0 "\/" v2) "/\" v1 ) or for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) )
assume A3: 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 v0, v1, v2 being Element of L st
( v0 "\/" v1 = v1 & not v0 "\/" (v2 "/\" v1) = (v0 "\/" v2) "/\" v1 ) or for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) )
assume A4: 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, v1, v2 being Element of L st
( v0 "\/" v1 = v1 & not v0 "\/" (v2 "/\" v1) = (v0 "\/" v2) "/\" v1 ) or for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) )
assume A5: 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, v1, v2 being Element of L st
( v0 "\/" v1 = v1 & not v0 "\/" (v2 "/\" v1) = (v0 "\/" v2) "/\" v1 ) or for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) )
assume A6: 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, v1, v2 being Element of L st
( v0 "\/" v1 = v1 & not v0 "\/" (v2 "/\" v1) = (v0 "\/" v2) "/\" v1 ) or for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) )
assume A7: 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, v1, v2 being Element of L st
( v0 "\/" v1 = v1 & not v0 "\/" (v2 "/\" v1) = (v0 "\/" v2) "/\" v1 ) or for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) )
assume A8: 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, v1, v2 being Element of L st
( v0 "\/" v1 = v1 & not v0 "\/" (v2 "/\" v1) = (v0 "\/" v2) "/\" v1 ) or for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) )
assume A9: for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) ; :: thesis: ( ex v0, v1, v2 being Element of L st
( v0 "\/" v1 = v1 & not v0 "\/" (v2 "/\" v1) = (v0 "\/" v2) "/\" v1 ) or for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) )
A11: 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 A4;
hence (v0 "\/" v1) "/\" (v0 "\/" (v1 "/\" v2)) = v0 "\/" (v1 "/\" v2) by A9; :: thesis: verum
end;
assume A12: for v0, v1, v2 being Element of L st v0 "\/" v1 = v1 holds
v0 "\/" (v2 "/\" v1) = (v0 "\/" v2) "/\" v1 ; :: thesis: for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3))
assume not for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) ; :: thesis: contradiction
then consider c1, c2, c3 being Element of L such that
A14: (c1 "/\" c2) "\/" (c1 "/\" c3) <> c1 "/\" (c2 "\/" (c1 "/\" c3)) ;
A17: 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 A8;
hence (v0 "/\" v1) "\/" (v0 "/\" (v1 "\/" v2)) = v0 "/\" (v1 "\/" v2) by A5; :: thesis: verum
end;
A20: 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 A2;
hence v101 "/\" v102 = v101 "/\" (v101 "/\" v102) by A3; :: thesis: verum
end;
A24: 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 A4;
hence (v1 "/\" v0) "/\" v2 = v0 "/\" (v1 "/\" v2) by A3; :: thesis: verum
end;
A27: 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 A3;
hence v0 "/\" (v1 "/\" v2) = v1 "/\" (v0 "/\" v2) by A24; :: thesis: verum
end;
A30: 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 A6;
hence v101 "\/" v102 = v101 "\/" (v101 "\/" v102) by A7; :: thesis: verum
end;
A35: 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 A6;
hence (v100 "\/" v102) "\/" v102 = v100 "\/" v102 by A7; :: thesis: verum
end;
A38: 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 A8;
hence v1 "\/" (v0 "\/" v1) = v0 "\/" v1 by A35; :: thesis: verum
end;
A41: 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 A8;
hence (v1 "\/" v0) "/\" (v0 "\/" (v1 "/\" v2)) = v0 "\/" (v1 "/\" v2) by A11; :: thesis: verum
end;
A45: for v2, v100 being Element of L holds (v100 "\/" v2) "/\" v100 = v100 "\/" (v2 "/\" v100)
proof
let v2, v100 be Element of L; :: thesis: (v100 "\/" v2) "/\" v100 = v100 "\/" (v2 "/\" v100)
( v100 "\/" v100 = v100 implies (v100 "\/" v2) "/\" v100 = v100 "\/" (v2 "/\" v100) ) by A12;
hence (v100 "\/" v2) "/\" v100 = v100 "\/" (v2 "/\" v100) by A6; :: thesis: verum
end;
A48: 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)
(v0 "\/" v1) "/\" v0 = v0 "/\" (v0 "\/" v1) by A4;
hence v0 "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v0) by A45; :: thesis: verum
end;
A52: 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 A20;
hence (v100 "/\" v1) "\/" (v100 "/\" ((v100 "/\" v1) "\/" v102)) = v100 "/\" ((v100 "/\" v1) "\/" v102) by A17; :: thesis: verum
end;
A56: for v101, v2, v100 being Element of L holds (v100 "\/" v2) "/\" (v100 "\/" v101) = v100 "\/" (v2 "/\" (v100 "\/" v101))
proof
let v101, v2, v100 be Element of L; :: thesis: (v100 "\/" v2) "/\" (v100 "\/" v101) = v100 "\/" (v2 "/\" (v100 "\/" v101))
( v100 "\/" (v100 "\/" v101) = v100 "\/" v101 implies (v100 "\/" v2) "/\" (v100 "\/" v101) = v100 "\/" (v2 "/\" (v100 "\/" v101)) ) by A12;
hence (v100 "\/" v2) "/\" (v100 "\/" v101) = v100 "\/" (v2 "/\" (v100 "\/" v101)) by A30; :: thesis: verum
end;
A60: for v101, v2, v100 being Element of L holds (v100 "\/" v2) "/\" (v101 "\/" v100) = v100 "\/" (v2 "/\" (v101 "\/" v100))
proof
let v101, v2, v100 be Element of L; :: thesis: (v100 "\/" v2) "/\" (v101 "\/" v100) = v100 "\/" (v2 "/\" (v101 "\/" v100))
( v100 "\/" (v101 "\/" v100) = v101 "\/" v100 implies (v100 "\/" v2) "/\" (v101 "\/" v100) = v100 "\/" (v2 "/\" (v101 "\/" v100)) ) by A12;
hence (v100 "\/" v2) "/\" (v101 "\/" v100) = v100 "\/" (v2 "/\" (v101 "\/" v100)) by A38; :: thesis: verum
end;
A63: 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 A4;
hence v0 "\/" (v0 "/\" v1) = v0 "/\" (v0 "\/" v1) by A48; :: thesis: verum
end;
A67: for v100, v1, v101 being Element of L holds v100 "/\" (v101 "\/" (v101 "/\" v1)) = v101 "/\" (v100 "/\" (v101 "\/" v1))
proof
let v100, v1, v101 be Element of L; :: thesis: v100 "/\" (v101 "\/" (v101 "/\" v1)) = v101 "/\" (v100 "/\" (v101 "\/" v1))
v101 "/\" (v101 "\/" v1) = v101 "\/" (v101 "/\" v1) by A63;
hence v100 "/\" (v101 "\/" (v101 "/\" v1)) = v101 "/\" (v100 "/\" (v101 "\/" v1)) by A27; :: thesis: verum
end;
A71: for v1, v2, v0 being Element of L holds v1 "\/" (v0 "/\" v2) = (v1 "\/" (v0 "/\" v2)) "/\" (v0 "\/" v1)
proof
let v1, v2, v0 be Element of L; :: thesis: v1 "\/" (v0 "/\" v2) = (v1 "\/" (v0 "/\" v2)) "/\" (v0 "\/" v1)
(v0 "\/" v1) "/\" (v1 "\/" (v0 "/\" v2)) = v1 "\/" (v0 "/\" v2) by A41;
hence v1 "\/" (v0 "/\" v2) = (v1 "\/" (v0 "/\" v2)) "/\" (v0 "\/" v1) by A4; :: thesis: verum
end;
A74: for v0, v2, v1 being Element of L holds v0 "\/" (v1 "/\" v2) = v0 "\/" ((v1 "/\" v2) "/\" (v1 "\/" v0))
proof
let v0, v2, v1 be Element of L; :: thesis: v0 "\/" (v1 "/\" v2) = v0 "\/" ((v1 "/\" v2) "/\" (v1 "\/" v0))
(v0 "\/" (v1 "/\" v2)) "/\" (v1 "\/" v0) = v0 "\/" ((v1 "/\" v2) "/\" (v1 "\/" v0)) by A60;
hence v0 "\/" (v1 "/\" v2) = v0 "\/" ((v1 "/\" v2) "/\" (v1 "\/" v0)) by A71; :: thesis: verum
end;
A76: for v0, v2, v1 being Element of L holds v0 "\/" (v1 "/\" v2) = v0 "\/" (v1 "/\" (v2 "/\" (v1 "\/" v0)))
proof
let v0, v2, v1 be Element of L; :: thesis: v0 "\/" (v1 "/\" v2) = v0 "\/" (v1 "/\" (v2 "/\" (v1 "\/" v0)))
(v1 "/\" v2) "/\" (v1 "\/" v0) = v1 "/\" (v2 "/\" (v1 "\/" v0)) by A3;
hence v0 "\/" (v1 "/\" v2) = v0 "\/" (v1 "/\" (v2 "/\" (v1 "\/" v0))) by A74; :: thesis: verum
end;
A79: for v2, v0, v1 being Element of L holds (v1 "\/" v0) "/\" (v0 "\/" v2) = v0 "\/" (v1 "/\" (v0 "\/" v2))
proof
let v2, v0, v1 be Element of L; :: thesis: (v1 "\/" v0) "/\" (v0 "\/" v2) = v0 "\/" (v1 "/\" (v0 "\/" v2))
v0 "\/" v1 = v1 "\/" v0 by A8;
hence (v1 "\/" v0) "/\" (v0 "\/" v2) = v0 "\/" (v1 "/\" (v0 "\/" v2)) by A56; :: thesis: verum
end;
A83: for v101, v2, v102 being Element of L holds ((v102 "/\" v2) "\/" v101) "/\" (v102 "\/" (v102 "/\" v2)) = (v102 "/\" v2) "\/" (v102 "/\" (v101 "/\" (v102 "\/" v2)))
proof
let v101, v2, v102 be Element of L; :: thesis: ((v102 "/\" v2) "\/" v101) "/\" (v102 "\/" (v102 "/\" v2)) = (v102 "/\" v2) "\/" (v102 "/\" (v101 "/\" (v102 "\/" v2)))
v101 "/\" (v102 "\/" (v102 "/\" v2)) = v102 "/\" (v101 "/\" (v102 "\/" v2)) by A67;
hence ((v102 "/\" v2) "\/" v101) "/\" (v102 "\/" (v102 "/\" v2)) = (v102 "/\" v2) "\/" (v102 "/\" (v101 "/\" (v102 "\/" v2))) by A60; :: thesis: verum
end;
A86: for v2, v1, v0 being Element of L holds (v0 "\/" (v0 "/\" v1)) "/\" ((v0 "/\" v1) "\/" v2) = (v0 "/\" v1) "\/" (v0 "/\" (v2 "/\" (v0 "\/" v1)))
proof
let v2, v1, v0 be Element of L; :: thesis: (v0 "\/" (v0 "/\" v1)) "/\" ((v0 "/\" v1) "\/" v2) = (v0 "/\" v1) "\/" (v0 "/\" (v2 "/\" (v0 "\/" v1)))
((v0 "/\" v1) "\/" v2) "/\" (v0 "\/" (v0 "/\" v1)) = (v0 "\/" (v0 "/\" v1)) "/\" ((v0 "/\" v1) "\/" v2) by A4;
hence (v0 "\/" (v0 "/\" v1)) "/\" ((v0 "/\" v1) "\/" v2) = (v0 "/\" v1) "\/" (v0 "/\" (v2 "/\" (v0 "\/" v1))) by A83; :: thesis: verum
end;
A88: for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" ((v0 "/\" v1) "\/" v2)) = (v0 "/\" v1) "\/" (v0 "/\" (v2 "/\" (v0 "\/" v1)))
proof
let v2, v1, v0 be Element of L; :: thesis: (v0 "/\" v1) "\/" (v0 "/\" ((v0 "/\" v1) "\/" v2)) = (v0 "/\" v1) "\/" (v0 "/\" (v2 "/\" (v0 "\/" v1)))
(v0 "\/" (v0 "/\" v1)) "/\" ((v0 "/\" v1) "\/" v2) = (v0 "/\" v1) "\/" (v0 "/\" ((v0 "/\" v1) "\/" v2)) by A79;
hence (v0 "/\" v1) "\/" (v0 "/\" ((v0 "/\" v1) "\/" v2)) = (v0 "/\" v1) "\/" (v0 "/\" (v2 "/\" (v0 "\/" v1))) by A86; :: thesis: verum
end;
A90: for v2, v1, v0 being Element of L holds v0 "/\" ((v0 "/\" v1) "\/" v2) = (v0 "/\" v1) "\/" (v0 "/\" (v2 "/\" (v0 "\/" v1)))
proof
let v2, v1, v0 be Element of L; :: thesis: v0 "/\" ((v0 "/\" v1) "\/" v2) = (v0 "/\" v1) "\/" (v0 "/\" (v2 "/\" (v0 "\/" v1)))
(v0 "/\" v1) "\/" (v0 "/\" ((v0 "/\" v1) "\/" v2)) = v0 "/\" ((v0 "/\" v1) "\/" v2) by A52;
hence v0 "/\" ((v0 "/\" v1) "\/" v2) = (v0 "/\" v1) "\/" (v0 "/\" (v2 "/\" (v0 "\/" v1))) by A88; :: thesis: verum
end;
A94: for v102, v2, v101 being Element of L holds (v101 "/\" v2) "\/" (v101 "/\" (v101 "/\" (v102 "/\" (v101 "\/" v2)))) = (v101 "/\" v2) "\/" (v101 "/\" v102)
proof
let v102, v2, v101 be Element of L; :: thesis: (v101 "/\" v2) "\/" (v101 "/\" (v101 "/\" (v102 "/\" (v101 "\/" v2)))) = (v101 "/\" v2) "\/" (v101 "/\" v102)
v102 "/\" (v101 "\/" (v101 "/\" v2)) = v101 "/\" (v102 "/\" (v101 "\/" v2)) by A67;
hence (v101 "/\" v2) "\/" (v101 "/\" (v101 "/\" (v102 "/\" (v101 "\/" v2)))) = (v101 "/\" v2) "\/" (v101 "/\" v102) by A76; :: thesis: verum
end;
A97: for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" (v2 "/\" (v0 "\/" v1))) = (v0 "/\" v1) "\/" (v0 "/\" v2)
proof
let v2, v1, v0 be Element of L; :: thesis: (v0 "/\" v1) "\/" (v0 "/\" (v2 "/\" (v0 "\/" v1))) = (v0 "/\" v1) "\/" (v0 "/\" v2)
v0 "/\" (v0 "/\" (v2 "/\" (v0 "\/" v1))) = v0 "/\" (v2 "/\" (v0 "\/" v1)) by A20;
hence (v0 "/\" v1) "\/" (v0 "/\" (v2 "/\" (v0 "\/" v1))) = (v0 "/\" v1) "\/" (v0 "/\" v2) by A94; :: thesis: verum
end;
A99: for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" v2) = v0 "/\" ((v0 "/\" v1) "\/" v2)
proof
let v2, v1, v0 be Element of L; :: thesis: (v0 "/\" v1) "\/" (v0 "/\" v2) = v0 "/\" ((v0 "/\" v1) "\/" v2)
(v0 "/\" v1) "\/" (v0 "/\" (v2 "/\" (v0 "\/" v1))) = (v0 "/\" v1) "\/" (v0 "/\" v2) by A97;
hence (v0 "/\" v1) "\/" (v0 "/\" v2) = v0 "/\" ((v0 "/\" v1) "\/" v2) by A90; :: thesis: verum
end;
A102: for v2, v1, v0 being Element of L holds v0 "/\" (v2 "\/" (v0 "/\" v1)) = (v0 "/\" v1) "\/" (v0 "/\" v2)
proof
let v2, v1, v0 be Element of L; :: thesis: v0 "/\" (v2 "\/" (v0 "/\" v1)) = (v0 "/\" v1) "\/" (v0 "/\" v2)
(v0 "/\" v1) "\/" v2 = v2 "\/" (v0 "/\" v1) by A8;
hence v0 "/\" (v2 "\/" (v0 "/\" v1)) = (v0 "/\" v1) "\/" (v0 "/\" v2) by A99; :: thesis: verum
end;
(c1 "/\" c3) "\/" (c1 "/\" c2) <> (c1 "/\" c2) "\/" (c1 "/\" c3) by A102, A14;
hence contradiction by A8; :: thesis: verum