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) "\/" v1 = ((v2 "\/" v1) "/\" v0) "\/" 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 v2, v1, v0 being Element of L st not ((v0 "\/" v1) "/\" v2) "\/" v1 = ((v2 "\/" v1) "/\" v0) "\/" 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 v2, v1, v0 being Element of L st not ((v0 "\/" v1) "/\" v2) "\/" v1 = ((v2 "\/" v1) "/\" v0) "\/" 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 v2, v1, v0 being Element of L st not ((v0 "\/" v1) "/\" v2) "\/" v1 = ((v2 "\/" v1) "/\" v0) "\/" 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 v2, v1, v0 being Element of L st not ((v0 "\/" v1) "/\" v2) "\/" v1 = ((v2 "\/" v1) "/\" v0) "\/" 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 v2, v1, v0 being Element of L st not ((v0 "\/" v1) "/\" v2) "\/" v1 = ((v2 "\/" v1) "/\" v0) "\/" 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 v2, v1, v0 being Element of L st not ((v0 "\/" v1) "/\" v2) "\/" v1 = ((v2 "\/" v1) "/\" v0) "\/" 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 v2, v1, v0 being Element of L st not ((v0 "\/" v1) "/\" v2) "\/" v1 = ((v2 "\/" v1) "/\" v0) "\/" 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 v2, v1, v0 being Element of L st not ((v0 "\/" v1) "/\" v2) "\/" v1 = ((v2 "\/" v1) "/\" v0) "\/" 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 v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" v2) "\/" v1 = ((v2 "\/" v1) "/\" v0) "\/" v1 ; :: thesis: for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3))
A14: for v2, v1, v0 being Element of L holds v1 "\/" ((v0 "\/" v1) "/\" v2) = ((v2 "\/" v1) "/\" v0) "\/" v1
proof
let v2, v1, v0 be Element of L; :: thesis: v1 "\/" ((v0 "\/" v1) "/\" v2) = ((v2 "\/" v1) "/\" v0) "\/" v1
((v0 "\/" v1) "/\" v2) "\/" v1 = v1 "\/" ((v0 "\/" v1) "/\" v2) by A8;
hence v1 "\/" ((v0 "\/" v1) "/\" v2) = ((v2 "\/" v1) "/\" v0) "\/" v1 by A12; :: thesis: verum
end;
A17: for v2, v0, v1 being Element of L holds v0 "\/" ((v1 "\/" v0) "/\" v2) = v0 "\/" ((v2 "\/" v0) "/\" v1)
proof
let v2, v0, v1 be Element of L; :: thesis: v0 "\/" ((v1 "\/" v0) "/\" v2) = v0 "\/" ((v2 "\/" v0) "/\" v1)
((v2 "\/" v0) "/\" v1) "\/" v0 = v0 "\/" ((v2 "\/" v0) "/\" v1) by A8;
hence v0 "\/" ((v1 "\/" v0) "/\" v2) = v0 "\/" ((v2 "\/" v0) "/\" v1) by A14; :: thesis: verum
end;
A21: 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;
A24: 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;
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 A4;
hence (v1 "/\" v0) "/\" v2 = v0 "/\" (v1 "/\" v2) by A3; :: 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 A3;
hence v0 "/\" (v1 "/\" v2) = v1 "/\" (v0 "/\" v2) by A28; :: thesis: verum
end;
A34: 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;
A37: 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 A34; :: thesis: verum
end;
A40: 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 A4;
hence (v0 "\/" v1) "/\" (v0 "\/" (v2 "/\" v1)) = v0 "\/" (v1 "/\" v2) by A11; :: thesis: verum
end;
A43: for v100, v101 being Element of L holds v100 "\/" (v101 "\/" v100) = v100 "\/" (((v101 "\/" v100) "\/" v100) "/\" v101)
proof
let v100, v101 be Element of L; :: thesis: v100 "\/" (v101 "\/" v100) = v100 "\/" (((v101 "\/" v100) "\/" v100) "/\" v101)
(v101 "\/" v100) "/\" (v101 "\/" v100) = v101 "\/" v100 by A2;
hence v100 "\/" (v101 "\/" v100) = v100 "\/" (((v101 "\/" v100) "\/" v100) "/\" v101) by A17; :: thesis: verum
end;
A46: for v0, v1 being Element of L holds v1 "\/" v0 = v0 "\/" (((v1 "\/" v0) "\/" v0) "/\" v1)
proof
let v0, v1 be Element of L; :: thesis: v1 "\/" v0 = v0 "\/" (((v1 "\/" v0) "\/" v0) "/\" v1)
v0 "\/" (v1 "\/" v0) = v1 "\/" v0 by A37;
hence v1 "\/" v0 = v0 "\/" (((v1 "\/" v0) "\/" v0) "/\" v1) by A43; :: thesis: verum
end;
A49: for v1, v0 being Element of L holds v0 "\/" v1 = v1 "\/" ((v1 "\/" (v0 "\/" v1)) "/\" v0)
proof
let v1, v0 be Element of L; :: thesis: v0 "\/" v1 = v1 "\/" ((v1 "\/" (v0 "\/" v1)) "/\" v0)
(v0 "\/" v1) "\/" v1 = v1 "\/" (v0 "\/" v1) by A8;
hence v0 "\/" v1 = v1 "\/" ((v1 "\/" (v0 "\/" v1)) "/\" v0) by A46; :: thesis: verum
end;
A51: 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)
v1 "\/" (v0 "\/" v1) = v0 "\/" v1 by A37;
hence v0 "\/" v1 = v1 "\/" ((v0 "\/" v1) "/\" v0) by A49; :: thesis: verum
end;
A53: for v1, v0 being Element of L holds v0 "\/" v1 = v1 "\/" (v0 "/\" (v0 "\/" v1))
proof
let v1, v0 be Element of L; :: thesis: v0 "\/" v1 = v1 "\/" (v0 "/\" (v0 "\/" v1))
(v0 "\/" v1) "/\" v0 = v0 "/\" (v0 "\/" v1) by A4;
hence v0 "\/" v1 = v1 "\/" (v0 "/\" (v0 "\/" v1)) by A51; :: thesis: verum
end;
A57: for v2, v0, v1 being Element of L holds v0 "\/" (v2 "/\" (v1 "\/" v0)) = v0 "\/" ((v2 "\/" v0) "/\" v1)
proof
let v2, v0, v1 be Element of L; :: thesis: v0 "\/" (v2 "/\" (v1 "\/" v0)) = v0 "\/" ((v2 "\/" v0) "/\" v1)
(v1 "\/" v0) "/\" v2 = v2 "/\" (v1 "\/" v0) by A4;
hence v0 "\/" (v2 "/\" (v1 "\/" v0)) = v0 "\/" ((v2 "\/" v0) "/\" v1) by A17; :: thesis: verum
end;
A62: for v102, v100 being Element of L holds v100 "\/" (v100 "/\" v102) = v100 "\/" ((v102 "\/" v100) "/\" v100)
proof
let v102, v100 be Element of L; :: thesis: v100 "\/" (v100 "/\" v102) = v100 "\/" ((v102 "\/" v100) "/\" v100)
v100 "\/" v100 = v100 by A6;
hence v100 "\/" (v100 "/\" v102) = v100 "\/" ((v102 "\/" v100) "/\" v100) by A17; :: thesis: verum
end;
A65: for v1, v0 being Element of L holds v0 "\/" (v0 "/\" v1) = v0 "\/" (v0 "/\" (v1 "\/" v0))
proof
let v1, v0 be Element of L; :: thesis: v0 "\/" (v0 "/\" v1) = v0 "\/" (v0 "/\" (v1 "\/" v0))
(v1 "\/" v0) "/\" v0 = v0 "/\" (v1 "\/" v0) by A4;
hence v0 "\/" (v0 "/\" v1) = v0 "\/" (v0 "/\" (v1 "\/" v0)) by A62; :: thesis: verum
end;
A69: for v102, v2, v100, v1 being Element of L holds (v100 "\/" ((v2 "\/" v100) "/\" v1)) "/\" (v100 "\/" (((v1 "\/" v100) "/\" v2) "/\" v102)) = v100 "\/" (((v1 "\/" v100) "/\" v2) "/\" v102)
proof
let v102, v2, v100, v1 be Element of L; :: thesis: (v100 "\/" ((v2 "\/" v100) "/\" v1)) "/\" (v100 "\/" (((v1 "\/" v100) "/\" v2) "/\" v102)) = v100 "\/" (((v1 "\/" v100) "/\" v2) "/\" v102)
v100 "\/" ((v1 "\/" v100) "/\" v2) = v100 "\/" ((v2 "\/" v100) "/\" v1) by A17;
hence (v100 "\/" ((v2 "\/" v100) "/\" v1)) "/\" (v100 "\/" (((v1 "\/" v100) "/\" v2) "/\" v102)) = v100 "\/" (((v1 "\/" v100) "/\" v2) "/\" v102) by A11; :: thesis: verum
end;
A72: for v3, v1, v0, v2 being Element of L holds (v0 "\/" (v1 "/\" (v2 "\/" v0))) "/\" (v0 "\/" (((v2 "\/" v0) "/\" v1) "/\" v3)) = v0 "\/" (((v2 "\/" v0) "/\" v1) "/\" v3)
proof
let v3, v1, v0, v2 be Element of L; :: thesis: (v0 "\/" (v1 "/\" (v2 "\/" v0))) "/\" (v0 "\/" (((v2 "\/" v0) "/\" v1) "/\" v3)) = v0 "\/" (((v2 "\/" v0) "/\" v1) "/\" v3)
v0 "\/" ((v1 "\/" v0) "/\" v2) = v0 "\/" (v1 "/\" (v2 "\/" v0)) by A57;
hence (v0 "\/" (v1 "/\" (v2 "\/" v0))) "/\" (v0 "\/" (((v2 "\/" v0) "/\" v1) "/\" v3)) = v0 "\/" (((v2 "\/" v0) "/\" v1) "/\" v3) by A69; :: thesis: verum
end;
A74: for v1, v3, v0, v2 being Element of L holds (v0 "\/" (v1 "/\" (v2 "\/" v0))) "/\" (v0 "\/" ((v2 "\/" v0) "/\" (v1 "/\" v3))) = v0 "\/" (((v2 "\/" v0) "/\" v1) "/\" v3)
proof
let v1, v3, v0, v2 be Element of L; :: thesis: (v0 "\/" (v1 "/\" (v2 "\/" v0))) "/\" (v0 "\/" ((v2 "\/" v0) "/\" (v1 "/\" v3))) = v0 "\/" (((v2 "\/" v0) "/\" v1) "/\" v3)
((v2 "\/" v0) "/\" v1) "/\" v3 = (v2 "\/" v0) "/\" (v1 "/\" v3) by A3;
hence (v0 "\/" (v1 "/\" (v2 "\/" v0))) "/\" (v0 "\/" ((v2 "\/" v0) "/\" (v1 "/\" v3))) = v0 "\/" (((v2 "\/" v0) "/\" v1) "/\" v3) by A72; :: thesis: verum
end;
A76: for v2, v0, v3, v1 being Element of L holds (v0 "\/" (v1 "/\" (v2 "\/" v0))) "/\" (v0 "\/" (v2 "/\" ((v1 "/\" v3) "\/" v0))) = v0 "\/" (((v2 "\/" v0) "/\" v1) "/\" v3)
proof
let v2, v0, v3, v1 be Element of L; :: thesis: (v0 "\/" (v1 "/\" (v2 "\/" v0))) "/\" (v0 "\/" (v2 "/\" ((v1 "/\" v3) "\/" v0))) = v0 "\/" (((v2 "\/" v0) "/\" v1) "/\" v3)
v0 "\/" ((v2 "\/" v0) "/\" (v1 "/\" v3)) = v0 "\/" (v2 "/\" ((v1 "/\" v3) "\/" v0)) by A57;
hence (v0 "\/" (v1 "/\" (v2 "\/" v0))) "/\" (v0 "\/" (v2 "/\" ((v1 "/\" v3) "\/" v0))) = v0 "\/" (((v2 "\/" v0) "/\" v1) "/\" v3) by A74; :: thesis: verum
end;
A78: for v2, v0, v3, v1 being Element of L holds (v0 "\/" (v1 "/\" (v2 "\/" v0))) "/\" (v0 "\/" (v2 "/\" ((v1 "/\" v3) "\/" v0))) = v0 "\/" ((v2 "\/" v0) "/\" (v1 "/\" v3))
proof
let v2, v0, v3, v1 be Element of L; :: thesis: (v0 "\/" (v1 "/\" (v2 "\/" v0))) "/\" (v0 "\/" (v2 "/\" ((v1 "/\" v3) "\/" v0))) = v0 "\/" ((v2 "\/" v0) "/\" (v1 "/\" v3))
((v2 "\/" v0) "/\" v1) "/\" v3 = (v2 "\/" v0) "/\" (v1 "/\" v3) by A3;
hence (v0 "\/" (v1 "/\" (v2 "\/" v0))) "/\" (v0 "\/" (v2 "/\" ((v1 "/\" v3) "\/" v0))) = v0 "\/" ((v2 "\/" v0) "/\" (v1 "/\" v3)) by A76; :: thesis: verum
end;
A80: for v2, v0, v3, v1 being Element of L holds (v0 "\/" (v1 "/\" (v2 "\/" v0))) "/\" (v0 "\/" (v2 "/\" ((v1 "/\" v3) "\/" v0))) = v0 "\/" (v2 "/\" ((v1 "/\" v3) "\/" v0))
proof
let v2, v0, v3, v1 be Element of L; :: thesis: (v0 "\/" (v1 "/\" (v2 "\/" v0))) "/\" (v0 "\/" (v2 "/\" ((v1 "/\" v3) "\/" v0))) = v0 "\/" (v2 "/\" ((v1 "/\" v3) "\/" v0))
v0 "\/" ((v2 "\/" v0) "/\" (v1 "/\" v3)) = v0 "\/" (v2 "/\" ((v1 "/\" v3) "\/" v0)) by A57;
hence (v0 "\/" (v1 "/\" (v2 "\/" v0))) "/\" (v0 "\/" (v2 "/\" ((v1 "/\" v3) "\/" v0))) = v0 "\/" (v2 "/\" ((v1 "/\" v3) "\/" v0)) by A78; :: thesis: verum
end;
A83: 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 A2;
hence v101 "\/" (v101 "/\" (v101 "\/" v102)) = v101 "/\" (v101 "\/" v102) by A21; :: thesis: verum
end;
A87: for v100, v101, v1 being Element of L holds (v100 "/\" v101) "\/" (v100 "/\" (v1 "\/" v101)) = v100 "/\" (v101 "\/" (v1 "\/" v101))
proof
let v100, v101, v1 be Element of L; :: thesis: (v100 "/\" v101) "\/" (v100 "/\" (v1 "\/" v101)) = v100 "/\" (v101 "\/" (v1 "\/" v101))
v101 "\/" (v1 "\/" v101) = v1 "\/" v101 by A37;
hence (v100 "/\" v101) "\/" (v100 "/\" (v1 "\/" v101)) = v100 "/\" (v101 "\/" (v1 "\/" v101)) by A21; :: thesis: verum
end;
A90: for v0, v1, v2 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" (v2 "\/" v1)) = v0 "/\" (v2 "\/" v1)
proof
let v0, v1, v2 be Element of L; :: thesis: (v0 "/\" v1) "\/" (v0 "/\" (v2 "\/" v1)) = v0 "/\" (v2 "\/" v1)
v1 "\/" (v2 "\/" v1) = v2 "\/" v1 by A37;
hence (v0 "/\" v1) "\/" (v0 "/\" (v2 "\/" v1)) = v0 "/\" (v2 "\/" v1) by A87; :: thesis: verum
end;
A93: for v101, v1 being Element of L holds (v1 "\/" v101) "\/" (v101 "/\" (v1 "\/" v101)) = v101 "\/" (v1 "\/" v101)
proof
let v101, v1 be Element of L; :: thesis: (v1 "\/" v101) "\/" (v101 "/\" (v1 "\/" v101)) = v101 "\/" (v1 "\/" v101)
v101 "\/" (v1 "\/" v101) = v1 "\/" v101 by A37;
hence (v1 "\/" v101) "\/" (v101 "/\" (v1 "\/" v101)) = v101 "\/" (v1 "\/" v101) by A53; :: thesis: verum
end;
A96: for v1, v0 being Element of L holds v0 "\/" (v1 "\/" (v1 "/\" (v0 "\/" v1))) = v1 "\/" (v0 "\/" v1)
proof
let v1, v0 be Element of L; :: thesis: v0 "\/" (v1 "\/" (v1 "/\" (v0 "\/" v1))) = v1 "\/" (v0 "\/" v1)
(v0 "\/" v1) "\/" (v1 "/\" (v0 "\/" v1)) = v0 "\/" (v1 "\/" (v1 "/\" (v0 "\/" v1))) by A7;
hence v0 "\/" (v1 "\/" (v1 "/\" (v0 "\/" v1))) = v1 "\/" (v0 "\/" v1) by A93; :: thesis: verum
end;
A98: for v0, v1 being Element of L holds v0 "\/" (v1 "\/" (v1 "/\" v0)) = v1 "\/" (v0 "\/" v1)
proof
let v0, v1 be Element of L; :: thesis: v0 "\/" (v1 "\/" (v1 "/\" v0)) = v1 "\/" (v0 "\/" v1)
v1 "\/" (v1 "/\" (v0 "\/" v1)) = v1 "\/" (v1 "/\" v0) by A65;
hence v0 "\/" (v1 "\/" (v1 "/\" v0)) = v1 "\/" (v0 "\/" v1) by A96; :: thesis: verum
end;
A100: for v0, v1 being Element of L holds v0 "\/" (v1 "\/" (v1 "/\" v0)) = v0 "\/" v1
proof
let v0, v1 be Element of L; :: thesis: v0 "\/" (v1 "\/" (v1 "/\" v0)) = v0 "\/" v1
v1 "\/" (v0 "\/" v1) = v0 "\/" v1 by A37;
hence v0 "\/" (v1 "\/" (v1 "/\" v0)) = v0 "\/" v1 by A98; :: thesis: verum
end;
A103: for v0, v100, v1 being Element of L holds v100 "\/" ((v0 "/\" v1) "\/" (v0 "/\" (v1 "/\" v100))) = v100 "\/" (v0 "/\" v1)
proof
let v0, v100, v1 be Element of L; :: thesis: v100 "\/" ((v0 "/\" v1) "\/" (v0 "/\" (v1 "/\" v100))) = v100 "\/" (v0 "/\" v1)
(v0 "/\" v1) "/\" v100 = v0 "/\" (v1 "/\" v100) by A3;
hence v100 "\/" ((v0 "/\" v1) "\/" (v0 "/\" (v1 "/\" v100))) = v100 "\/" (v0 "/\" v1) by A100; :: thesis: verum
end;
A106: for v1, v0 being Element of L holds v0 "\/" (v0 "/\" (v0 "\/" v1)) = v0 "\/" (v0 "/\" v1)
proof
let v1, v0 be Element of L; :: thesis: v0 "\/" (v0 "/\" (v0 "\/" v1)) = v0 "\/" (v0 "/\" v1)
v1 "\/" v0 = v0 "\/" v1 by A8;
hence v0 "\/" (v0 "/\" (v0 "\/" v1)) = v0 "\/" (v0 "/\" v1) by A65; :: thesis: verum
end;
A108: 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 A83;
hence v0 "/\" (v0 "\/" v1) = v0 "\/" (v0 "/\" v1) by A106; :: thesis: verum
end;
A111: 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 A108;
hence v100 "/\" (v101 "\/" (v101 "/\" v1)) = v101 "/\" (v100 "/\" (v101 "\/" v1)) by A31; :: thesis: verum
end;
A115: for v1, v100, v101 being Element of L holds (v100 "\/" v101) "/\" (v100 "\/" (v1 "/\" (v101 "\/" v100))) = v100 "\/" (v101 "/\" (v1 "\/" v100))
proof
let v1, v100, v101 be Element of L; :: thesis: (v100 "\/" v101) "/\" (v100 "\/" (v1 "/\" (v101 "\/" v100))) = v100 "\/" (v101 "/\" (v1 "\/" v100))
v100 "\/" ((v1 "\/" v100) "/\" v101) = v100 "\/" (v1 "/\" (v101 "\/" v100)) by A57;
hence (v100 "\/" v101) "/\" (v100 "\/" (v1 "/\" (v101 "\/" v100))) = v100 "\/" (v101 "/\" (v1 "\/" v100)) by A40; :: thesis: verum
end;
A119: for v102, v1, v100 being Element of L holds (v100 "/\" v1) "\/" (v100 "/\" (v102 "\/" (v100 "/\" v1))) = v100 "/\" (v102 "\/" (v100 "/\" v1))
proof
let v102, v1, v100 be Element of L; :: thesis: (v100 "/\" v1) "\/" (v100 "/\" (v102 "\/" (v100 "/\" v1))) = v100 "/\" (v102 "\/" (v100 "/\" v1))
v100 "/\" (v100 "/\" v1) = v100 "/\" v1 by A24;
hence (v100 "/\" v1) "\/" (v100 "/\" (v102 "\/" (v100 "/\" v1))) = v100 "/\" (v102 "\/" (v100 "/\" v1)) by A90; :: thesis: verum
end;
A123: for v100, v103, v101 being Element of L holds (v100 "\/" (v101 "/\" ((v101 "/\" v103) "\/" v100))) "/\" (v100 "\/" ((v101 "/\" v103) "\/" ((v101 "/\" v103) "/\" v100))) = v100 "\/" ((v101 "/\" v103) "/\" ((v101 "/\" v103) "\/" v100))
proof
let v100, v103, v101 be Element of L; :: thesis: (v100 "\/" (v101 "/\" ((v101 "/\" v103) "\/" v100))) "/\" (v100 "\/" ((v101 "/\" v103) "\/" ((v101 "/\" v103) "/\" v100))) = v100 "\/" ((v101 "/\" v103) "/\" ((v101 "/\" v103) "\/" v100))
(v101 "/\" v103) "/\" ((v101 "/\" v103) "\/" v100) = (v101 "/\" v103) "\/" ((v101 "/\" v103) "/\" v100) by A108;
hence (v100 "\/" (v101 "/\" ((v101 "/\" v103) "\/" v100))) "/\" (v100 "\/" ((v101 "/\" v103) "\/" ((v101 "/\" v103) "/\" v100))) = v100 "\/" ((v101 "/\" v103) "/\" ((v101 "/\" v103) "\/" v100)) by A80; :: thesis: verum
end;
A126: for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" ((v1 "/\" v2) "\/" v0))) "/\" (v0 "\/" ((v1 "/\" v2) "\/" (v1 "/\" (v2 "/\" v0)))) = v0 "\/" ((v1 "/\" v2) "/\" ((v1 "/\" v2) "\/" v0))
proof
let v0, v2, v1 be Element of L; :: thesis: (v0 "\/" (v1 "/\" ((v1 "/\" v2) "\/" v0))) "/\" (v0 "\/" ((v1 "/\" v2) "\/" (v1 "/\" (v2 "/\" v0)))) = v0 "\/" ((v1 "/\" v2) "/\" ((v1 "/\" v2) "\/" v0))
(v1 "/\" v2) "/\" v0 = v1 "/\" (v2 "/\" v0) by A3;
hence (v0 "\/" (v1 "/\" ((v1 "/\" v2) "\/" v0))) "/\" (v0 "\/" ((v1 "/\" v2) "\/" (v1 "/\" (v2 "/\" v0)))) = v0 "\/" ((v1 "/\" v2) "/\" ((v1 "/\" v2) "\/" v0)) by A123; :: thesis: verum
end;
A128: for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" ((v1 "/\" v2) "\/" v0))) "/\" (v0 "\/" (v1 "/\" v2)) = v0 "\/" ((v1 "/\" v2) "/\" ((v1 "/\" v2) "\/" v0))
proof
let v0, v2, v1 be Element of L; :: thesis: (v0 "\/" (v1 "/\" ((v1 "/\" v2) "\/" v0))) "/\" (v0 "\/" (v1 "/\" v2)) = v0 "\/" ((v1 "/\" v2) "/\" ((v1 "/\" v2) "\/" v0))
v0 "\/" ((v1 "/\" v2) "\/" (v1 "/\" (v2 "/\" v0))) = v0 "\/" (v1 "/\" v2) by A103;
hence (v0 "\/" (v1 "/\" ((v1 "/\" v2) "\/" v0))) "/\" (v0 "\/" (v1 "/\" v2)) = v0 "\/" ((v1 "/\" v2) "/\" ((v1 "/\" v2) "\/" v0)) by A126; :: thesis: verum
end;
A130: for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" (v1 "/\" ((v1 "/\" v2) "\/" v0))) = v0 "\/" ((v1 "/\" v2) "/\" ((v1 "/\" v2) "\/" v0))
proof
let v0, v2, v1 be Element of L; :: thesis: (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" (v1 "/\" ((v1 "/\" v2) "\/" v0))) = v0 "\/" ((v1 "/\" v2) "/\" ((v1 "/\" v2) "\/" v0))
(v0 "\/" (v1 "/\" ((v1 "/\" v2) "\/" v0))) "/\" (v0 "\/" (v1 "/\" v2)) = (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" (v1 "/\" ((v1 "/\" v2) "\/" v0))) by A4;
hence (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" (v1 "/\" ((v1 "/\" v2) "\/" v0))) = v0 "\/" ((v1 "/\" v2) "/\" ((v1 "/\" v2) "\/" v0)) by A128; :: thesis: verum
end;
A132: for v0, v2, v1 being Element of L holds v0 "\/" ((v1 "/\" v2) "/\" (v1 "\/" v0)) = v0 "\/" ((v1 "/\" v2) "/\" ((v1 "/\" v2) "\/" v0))
proof
let v0, v2, v1 be Element of L; :: thesis: v0 "\/" ((v1 "/\" v2) "/\" (v1 "\/" v0)) = v0 "\/" ((v1 "/\" v2) "/\" ((v1 "/\" v2) "\/" v0))
(v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" (v1 "/\" ((v1 "/\" v2) "\/" v0))) = v0 "\/" ((v1 "/\" v2) "/\" (v1 "\/" v0)) by A115;
hence v0 "\/" ((v1 "/\" v2) "/\" (v1 "\/" v0)) = v0 "\/" ((v1 "/\" v2) "/\" ((v1 "/\" v2) "\/" v0)) by A130; :: thesis: verum
end;
A134: for v2, v0, v1 being Element of L holds v0 "\/" (v1 "/\" (v2 "/\" (v1 "\/" v0))) = v0 "\/" ((v1 "/\" v2) "/\" ((v1 "/\" v2) "\/" v0))
proof
let v2, v0, v1 be Element of L; :: thesis: v0 "\/" (v1 "/\" (v2 "/\" (v1 "\/" v0))) = v0 "\/" ((v1 "/\" v2) "/\" ((v1 "/\" v2) "\/" v0))
(v1 "/\" v2) "/\" (v1 "\/" v0) = v1 "/\" (v2 "/\" (v1 "\/" v0)) by A3;
hence v0 "\/" (v1 "/\" (v2 "/\" (v1 "\/" v0))) = v0 "\/" ((v1 "/\" v2) "/\" ((v1 "/\" v2) "\/" v0)) by A132; :: thesis: verum
end;
A136: for v2, v0, v1 being Element of L holds v0 "\/" (v1 "/\" (v2 "/\" (v1 "\/" v0))) = v0 "\/" ((v1 "/\" v2) "\/" ((v1 "/\" v2) "/\" v0))
proof
let v2, v0, v1 be Element of L; :: thesis: v0 "\/" (v1 "/\" (v2 "/\" (v1 "\/" v0))) = v0 "\/" ((v1 "/\" v2) "\/" ((v1 "/\" v2) "/\" v0))
(v1 "/\" v2) "/\" ((v1 "/\" v2) "\/" v0) = (v1 "/\" v2) "\/" ((v1 "/\" v2) "/\" v0) by A108;
hence v0 "\/" (v1 "/\" (v2 "/\" (v1 "\/" v0))) = v0 "\/" ((v1 "/\" v2) "\/" ((v1 "/\" v2) "/\" v0)) by A134; :: thesis: verum
end;
A138: for v2, v0, v1 being Element of L holds v0 "\/" (v1 "/\" (v2 "/\" (v1 "\/" v0))) = v0 "\/" ((v1 "/\" v2) "\/" (v1 "/\" (v2 "/\" v0)))
proof
let v2, v0, v1 be Element of L; :: thesis: v0 "\/" (v1 "/\" (v2 "/\" (v1 "\/" v0))) = v0 "\/" ((v1 "/\" v2) "\/" (v1 "/\" (v2 "/\" v0)))
(v1 "/\" v2) "/\" v0 = v1 "/\" (v2 "/\" v0) by A3;
hence v0 "\/" (v1 "/\" (v2 "/\" (v1 "\/" v0))) = v0 "\/" ((v1 "/\" v2) "\/" (v1 "/\" (v2 "/\" v0))) by A136; :: thesis: verum
end;
A140: for v2, v0, v1 being Element of L holds v0 "\/" (v1 "/\" (v2 "/\" (v1 "\/" v0))) = v0 "\/" (v1 "/\" v2)
proof
let v2, v0, v1 be Element of L; :: thesis: v0 "\/" (v1 "/\" (v2 "/\" (v1 "\/" v0))) = v0 "\/" (v1 "/\" v2)
v0 "\/" ((v1 "/\" v2) "\/" (v1 "/\" (v2 "/\" v0))) = v0 "\/" (v1 "/\" v2) by A103;
hence v0 "\/" (v1 "/\" (v2 "/\" (v1 "\/" v0))) = v0 "\/" (v1 "/\" v2) by A138; :: thesis: verum
end;
A143: for v101, v2, v102 being Element of L holds (v102 "/\" v2) "\/" ((v101 "\/" (v102 "/\" v2)) "/\" v102) = (v102 "/\" v2) "\/" (v102 "/\" (v101 "/\" (v102 "\/" v2)))
proof
let v101, v2, v102 be Element of L; :: thesis: (v102 "/\" v2) "\/" ((v101 "\/" (v102 "/\" v2)) "/\" v102) = (v102 "/\" v2) "\/" (v102 "/\" (v101 "/\" (v102 "\/" v2)))
v101 "/\" (v102 "\/" (v102 "/\" v2)) = v102 "/\" (v101 "/\" (v102 "\/" v2)) by A111;
hence (v102 "/\" v2) "\/" ((v101 "\/" (v102 "/\" v2)) "/\" v102) = (v102 "/\" v2) "\/" (v102 "/\" (v101 "/\" (v102 "\/" v2))) by A57; :: thesis: verum
end;
A146: for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" (v2 "\/" (v0 "/\" v1))) = (v0 "/\" v1) "\/" (v0 "/\" (v2 "/\" (v0 "\/" v1)))
proof
let v2, v1, v0 be Element of L; :: thesis: (v0 "/\" v1) "\/" (v0 "/\" (v2 "\/" (v0 "/\" v1))) = (v0 "/\" v1) "\/" (v0 "/\" (v2 "/\" (v0 "\/" v1)))
(v2 "\/" (v0 "/\" v1)) "/\" v0 = v0 "/\" (v2 "\/" (v0 "/\" v1)) by A4;
hence (v0 "/\" v1) "\/" (v0 "/\" (v2 "\/" (v0 "/\" v1))) = (v0 "/\" v1) "\/" (v0 "/\" (v2 "/\" (v0 "\/" v1))) by A143; :: thesis: verum
end;
A148: for v2, v1, v0 being Element of L holds v0 "/\" (v2 "\/" (v0 "/\" v1)) = (v0 "/\" v1) "\/" (v0 "/\" (v2 "/\" (v0 "\/" v1)))
proof
let v2, v1, v0 be Element of L; :: thesis: v0 "/\" (v2 "\/" (v0 "/\" v1)) = (v0 "/\" v1) "\/" (v0 "/\" (v2 "/\" (v0 "\/" v1)))
(v0 "/\" v1) "\/" (v0 "/\" (v2 "\/" (v0 "/\" v1))) = v0 "/\" (v2 "\/" (v0 "/\" v1)) by A119;
hence v0 "/\" (v2 "\/" (v0 "/\" v1)) = (v0 "/\" v1) "\/" (v0 "/\" (v2 "/\" (v0 "\/" v1))) by A146; :: thesis: verum
end;
A154: 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 A111;
hence (v101 "/\" v2) "\/" (v101 "/\" (v101 "/\" (v102 "/\" (v101 "\/" v2)))) = (v101 "/\" v2) "\/" (v101 "/\" v102) by A140; :: thesis: verum
end;
A157: 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 A24;
hence (v0 "/\" v1) "\/" (v0 "/\" (v2 "/\" (v0 "\/" v1))) = (v0 "/\" v1) "\/" (v0 "/\" v2) by A154; :: thesis: verum
end;
A159: for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" v2) = v0 "/\" (v2 "\/" (v0 "/\" v1))
proof
let v2, v1, v0 be Element of L; :: thesis: (v0 "/\" v1) "\/" (v0 "/\" v2) = v0 "/\" (v2 "\/" (v0 "/\" v1))
(v0 "/\" v1) "\/" (v0 "/\" (v2 "/\" (v0 "\/" v1))) = (v0 "/\" v1) "\/" (v0 "/\" v2) by A157;
hence (v0 "/\" v1) "\/" (v0 "/\" v2) = v0 "/\" (v2 "\/" (v0 "/\" v1)) by A148; :: thesis: verum
end;
let v1, v2, v3 be Element of L; :: thesis: (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3))
v1 "/\" (v2 "\/" (v1 "/\" v3)) = (v1 "/\" v3) "\/" (v1 "/\" v2) by A159;
hence (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) by A8; :: thesis: verum