let L be non empty LattStr ; :: thesis: ( ( 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) "\/" (v0 "/\" v2) = v0 "/\" (v1 "\/" (v0 "/\" v2)) ) implies for v1, v2, v3 being Element of L st v1 "\/" v2 = v2 holds
v1 "\/" (v3 "/\" v2) = (v1 "\/" v3) "/\" v2 )
assume A1: 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) "\/" (v0 "/\" v2) = v0 "/\" (v1 "\/" (v0 "/\" v2)) or for v1, v2, v3 being Element of L st v1 "\/" v2 = v2 holds
v1 "\/" (v3 "/\" v2) = (v1 "\/" v3) "/\" v2 )
assume A2: 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) "\/" (v0 "/\" v2) = v0 "/\" (v1 "\/" (v0 "/\" v2)) or for v1, v2, v3 being Element of L st v1 "\/" v2 = v2 holds
v1 "\/" (v3 "/\" v2) = (v1 "\/" v3) "/\" v2 )
assume A3: 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) "\/" (v0 "/\" v2) = v0 "/\" (v1 "\/" (v0 "/\" v2)) or for v1, v2, v3 being Element of L st v1 "\/" v2 = v2 holds
v1 "\/" (v3 "/\" v2) = (v1 "\/" v3) "/\" v2 )
assume A4: 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) "\/" (v0 "/\" v2) = v0 "/\" (v1 "\/" (v0 "/\" v2)) or for v1, v2, v3 being Element of L st v1 "\/" v2 = v2 holds
v1 "\/" (v3 "/\" v2) = (v1 "\/" v3) "/\" v2 )
assume A5: 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) "\/" (v0 "/\" v2) = v0 "/\" (v1 "\/" (v0 "/\" v2)) or for v1, v2, v3 being Element of L st v1 "\/" v2 = v2 holds
v1 "\/" (v3 "/\" v2) = (v1 "\/" v3) "/\" v2 )
assume A6: 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) "\/" (v0 "/\" v2) = v0 "/\" (v1 "\/" (v0 "/\" v2)) or for v1, v2, v3 being Element of L st v1 "\/" v2 = v2 holds
v1 "\/" (v3 "/\" v2) = (v1 "\/" v3) "/\" v2 )
A8: 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 A1;
hence (v0 "\/" v1) "/\" (v0 "\/" (v1 "/\" v2)) = v0 "\/" (v1 "/\" v2) by A6; :: thesis: verum
end;
assume A9: for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" v2) = v0 "/\" (v1 "\/" (v0 "/\" v2)) ; :: thesis: for v1, v2, v3 being Element of L st v1 "\/" v2 = v2 holds
v1 "\/" (v3 "/\" v2) = (v1 "\/" v3) "/\" v2
assume ex v1, v2, v3 being Element of L st
( v1 "\/" v2 = v2 & not v1 "\/" (v3 "/\" v2) = (v1 "\/" v3) "/\" v2 ) ; :: thesis: contradiction
then consider c1, c2, c3 being Element of L such that
A10: c1 "\/" c2 = c2 and
A11: c1 "\/" (c3 "/\" c2) <> (c1 "\/" c3) "/\" c2 ;
c1 "\/" (c2 "/\" c3) <> (c1 "\/" c3) "/\" c2 by A1, A11;
then A15: c1 "\/" (c2 "/\" c3) <> c2 "/\" (c1 "\/" c3) by A1;
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 A5;
hence (v0 "/\" v1) "\/" (v0 "/\" (v1 "\/" v2)) = v0 "/\" (v1 "\/" v2) by A2; :: thesis: verum
end;
A19: 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) "\/" (v0 "/\" (v1 "\/" v2)) = v0 "/\" (v1 "\/" (v0 "/\" (v1 "\/" v2))) by A9;
hence v0 "/\" (v1 "\/" (v0 "/\" (v1 "\/" v2))) = v0 "/\" (v1 "\/" v2) by A17; :: thesis: verum
end;
A22: 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 A3;
hence v101 "\/" v102 = v101 "\/" (v101 "\/" v102) by A4; :: thesis: verum
end;
A27: for v1, v2, v0 being Element of L holds v0 "/\" (v1 "\/" (v0 "/\" v2)) = (v0 "/\" v2) "\/" (v0 "/\" v1)
proof
let v1, v2, v0 be Element of L; :: thesis: v0 "/\" (v1 "\/" (v0 "/\" v2)) = (v0 "/\" v2) "\/" (v0 "/\" v1)
(v0 "/\" v1) "\/" (v0 "/\" v2) = v0 "/\" (v1 "\/" (v0 "/\" v2)) by A9;
hence v0 "/\" (v1 "\/" (v0 "/\" v2)) = (v0 "/\" v2) "\/" (v0 "/\" v1) by A5; :: thesis: verum
end;
A29: for v1, v2, v0 being Element of L holds v0 "/\" (v1 "\/" (v0 "/\" v2)) = v0 "/\" (v2 "\/" (v0 "/\" v1))
proof
let v1, v2, v0 be Element of L; :: thesis: v0 "/\" (v1 "\/" (v0 "/\" v2)) = v0 "/\" (v2 "\/" (v0 "/\" v1))
(v0 "/\" v2) "\/" (v0 "/\" v1) = v0 "/\" (v2 "\/" (v0 "/\" v1)) by A9;
hence v0 "/\" (v1 "\/" (v0 "/\" v2)) = v0 "/\" (v2 "\/" (v0 "/\" v1)) by A27; :: thesis: verum
end;
A35: for v102 being Element of L holds c1 "\/" (c2 "/\" (c1 "\/" v102)) = c2 "/\" (c1 "\/" v102)
proof
let v102 be Element of L; :: thesis: c1 "\/" (c2 "/\" (c1 "\/" v102)) = c2 "/\" (c1 "\/" v102)
c2 "/\" (c1 "\/" (c2 "/\" (c1 "\/" v102))) = c1 "\/" (c2 "/\" (c1 "\/" v102)) by A10, A8;
hence c1 "\/" (c2 "/\" (c1 "\/" v102)) = c2 "/\" (c1 "\/" v102) by A19; :: thesis: verum
end;
A38: for v0 being Element of L holds c1 "\/" (c2 "/\" (v0 "\/" c1)) = c2 "/\" (c1 "\/" v0)
proof
let v0 be Element of L; :: thesis: c1 "\/" (c2 "/\" (v0 "\/" c1)) = c2 "/\" (c1 "\/" v0)
c1 "\/" v0 = v0 "\/" c1 by A5;
hence c1 "\/" (c2 "/\" (v0 "\/" c1)) = c2 "/\" (c1 "\/" v0) by A35; :: thesis: verum
end;
A40: for v0, v2, v1 being Element of L holds v0 "/\" ((v1 "\/" v2) "\/" (v0 "/\" v1)) = v0 "/\" (v1 "\/" v2)
proof
let v0, v2, v1 be Element of L; :: thesis: v0 "/\" ((v1 "\/" v2) "\/" (v0 "/\" v1)) = v0 "/\" (v1 "\/" v2)
v0 "/\" (v1 "\/" (v0 "/\" (v1 "\/" v2))) = v0 "/\" ((v1 "\/" v2) "\/" (v0 "/\" v1)) by A29;
hence v0 "/\" ((v1 "\/" v2) "\/" (v0 "/\" v1)) = v0 "/\" (v1 "\/" v2) by A19; :: thesis: verum
end;
A42: for v2, v1, v0 being Element of L holds v0 "/\" (v1 "\/" (v2 "\/" (v0 "/\" v1))) = v0 "/\" (v1 "\/" v2)
proof
let v2, v1, v0 be Element of L; :: thesis: v0 "/\" (v1 "\/" (v2 "\/" (v0 "/\" v1))) = v0 "/\" (v1 "\/" v2)
(v1 "\/" v2) "\/" (v0 "/\" v1) = v1 "\/" (v2 "\/" (v0 "/\" v1)) by A4;
hence v0 "/\" (v1 "\/" (v2 "\/" (v0 "/\" v1))) = v0 "/\" (v1 "\/" v2) by A40; :: thesis: verum
end;
A44: for v0 being Element of L holds c2 "/\" (v0 "\/" (c2 "/\" c1)) = c1 "\/" (c2 "/\" v0)
proof
let v0 be Element of L; :: thesis: c2 "/\" (v0 "\/" (c2 "/\" c1)) = c1 "\/" (c2 "/\" v0)
c2 "/\" (c1 "\/" (c2 "/\" v0)) = c2 "/\" (v0 "\/" (c2 "/\" c1)) by A29;
hence c2 "/\" (v0 "\/" (c2 "/\" c1)) = c1 "\/" (c2 "/\" v0) by A10, A8; :: thesis: verum
end;
A45: c2 "/\" c1 = c1 "/\" c2 by A1;
A50: for v101 being Element of L holds c2 "/\" (v101 "\/" (c1 "\/" (c2 "/\" v101))) = c2 "/\" (v101 "\/" (c1 "/\" c2))
proof
let v101 be Element of L; :: thesis: c2 "/\" (v101 "\/" (c1 "\/" (c2 "/\" v101))) = c2 "/\" (v101 "\/" (c1 "/\" c2))
c1 "\/" (c2 "/\" v101) = c2 "/\" (v101 "\/" (c1 "/\" c2)) by A45, A44;
hence c2 "/\" (v101 "\/" (c1 "\/" (c2 "/\" v101))) = c2 "/\" (v101 "\/" (c1 "/\" c2)) by A19; :: thesis: verum
end;
A53: for v0 being Element of L holds c2 "/\" (v0 "\/" c1) = c2 "/\" (v0 "\/" (c1 "/\" c2))
proof
let v0 be Element of L; :: thesis: c2 "/\" (v0 "\/" c1) = c2 "/\" (v0 "\/" (c1 "/\" c2))
c2 "/\" (v0 "\/" (c1 "\/" (c2 "/\" v0))) = c2 "/\" (v0 "\/" c1) by A42;
hence c2 "/\" (v0 "\/" c1) = c2 "/\" (v0 "\/" (c1 "/\" c2)) by A50; :: thesis: verum
end;
A57: for v0 being Element of L holds c1 "\/" (c2 "/\" (v0 "\/" (c1 "/\" c2))) = c1 "\/" (c2 "/\" v0)
proof
let v0 be Element of L; :: thesis: c1 "\/" (c2 "/\" (v0 "\/" (c1 "/\" c2))) = c1 "\/" (c2 "/\" v0)
c1 "\/" (c2 "/\" v0) = c2 "/\" (v0 "\/" (c1 "/\" c2)) by A45, A44;
hence c1 "\/" (c2 "/\" (v0 "\/" (c1 "/\" c2))) = c1 "\/" (c2 "/\" v0) by A22; :: thesis: verum
end;
A59: for v0 being Element of L holds c1 "\/" (c2 "/\" (v0 "\/" c1)) = c1 "\/" (c2 "/\" v0)
proof
let v0 be Element of L; :: thesis: c1 "\/" (c2 "/\" (v0 "\/" c1)) = c1 "\/" (c2 "/\" v0)
c2 "/\" (v0 "\/" (c1 "/\" c2)) = c2 "/\" (v0 "\/" c1) by A53;
hence c1 "\/" (c2 "/\" (v0 "\/" c1)) = c1 "\/" (c2 "/\" v0) by A57; :: thesis: verum
end;
for v0 being Element of L holds c2 "/\" (c1 "\/" v0) = c1 "\/" (c2 "/\" v0)
proof
let v0 be Element of L; :: thesis: c2 "/\" (c1 "\/" v0) = c1 "\/" (c2 "/\" v0)
c1 "\/" (c2 "/\" (v0 "\/" c1)) = c2 "/\" (c1 "\/" v0) by A38;
hence c2 "/\" (c1 "\/" v0) = c1 "\/" (c2 "/\" v0) by A59; :: thesis: verum
end;
hence contradiction by A15; :: thesis: verum