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 being Element of L holds v0 "\/" v0 = v0 ) & ( for v1, v0 being Element of L holds v0 "\/" v1 = v1 "\/" v0 ) & ( for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" (v2 "\/" v1)) "/\" v1 = v1 ) & ( for v2, v1, v0 being Element of L holds ((v0 "/\" v1) "\/" (v2 "/\" v1)) "\/" v1 = v1 ) & ( for v1, v2, v0 being Element of L holds v0 "/\" (v1 "\/" (v0 "\/" v2)) = v0 ) implies for v0, v1, v2 being Element of L holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) )
assume A2: 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 being Element of L st not v0 "\/" v0 = v0 or ex v1, v0 being Element of L st not v0 "\/" v1 = v1 "\/" v0 or ex v2, v1, v0 being Element of L st not ((v0 "\/" v1) "/\" (v2 "\/" v1)) "/\" v1 = v1 or ex v2, v1, v0 being Element of L st not ((v0 "/\" v1) "\/" (v2 "/\" v1)) "\/" v1 = v1 or ex v1, v2, v0 being Element of L st not v0 "/\" (v1 "\/" (v0 "\/" v2)) = v0 or for v0, v1, v2 being Element of L holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) )
assume A3: for v1, v0 being Element of L holds v0 "/\" v1 = v1 "/\" v0 ; :: thesis: ( ex v0 being Element of L st not v0 "\/" v0 = v0 or ex v1, v0 being Element of L st not v0 "\/" v1 = v1 "\/" v0 or ex v2, v1, v0 being Element of L st not ((v0 "\/" v1) "/\" (v2 "\/" v1)) "/\" v1 = v1 or ex v2, v1, v0 being Element of L st not ((v0 "/\" v1) "\/" (v2 "/\" v1)) "\/" v1 = v1 or ex v1, v2, v0 being Element of L st not v0 "/\" (v1 "\/" (v0 "\/" v2)) = v0 or for v0, v1, v2 being Element of L holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) )
assume A4: 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 v2, v1, v0 being Element of L st not ((v0 "\/" v1) "/\" (v2 "\/" v1)) "/\" v1 = v1 or ex v2, v1, v0 being Element of L st not ((v0 "/\" v1) "\/" (v2 "/\" v1)) "\/" v1 = v1 or ex v1, v2, v0 being Element of L st not v0 "/\" (v1 "\/" (v0 "\/" v2)) = v0 or for v0, v1, v2 being Element of L holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) )
assume A5: for v1, v0 being Element of L holds v0 "\/" v1 = v1 "\/" v0 ; :: thesis: ( ex v2, v1, v0 being Element of L st not ((v0 "\/" v1) "/\" (v2 "\/" v1)) "/\" v1 = v1 or ex v2, v1, v0 being Element of L st not ((v0 "/\" v1) "\/" (v2 "/\" v1)) "\/" v1 = v1 or ex v1, v2, v0 being Element of L st not v0 "/\" (v1 "\/" (v0 "\/" v2)) = v0 or for v0, v1, v2 being Element of L holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) )
assume A6: for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" (v2 "\/" v1)) "/\" v1 = v1 ; :: thesis: ( ex v2, v1, v0 being Element of L st not ((v0 "/\" v1) "\/" (v2 "/\" v1)) "\/" v1 = v1 or ex v1, v2, v0 being Element of L st not v0 "/\" (v1 "\/" (v0 "\/" v2)) = v0 or for v0, v1, v2 being Element of L holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) )
A8: for v2, v1, v0 being Element of L holds v1 "/\" ((v0 "\/" v1) "/\" (v2 "\/" v1)) = v1

proof

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

end;

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

proof

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

end;

assume A14: for v1, v2, v0 being Element of L holds v0 "/\" (v1 "\/" (v0 "\/" v2)) = v0 ; :: thesis: for v0, v1, v2 being Element of L holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2)
A20: for v100, v102 being Element of L holds v100 "/\" (v102 "\/" v100) = v100

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

let v101, v1, v2, v102 be Element of L; :: thesis: (v1 "\/" (v102 "\/" v2)) "\/" (((v1 "\/" (v102 "\/" v2)) "/\" v101) "\/" v102) = v1 "\/" (v102 "\/" v2)
v102 "/\" (v1 "\/" (v102 "\/" v2)) = v102 by A14;
hence (v1 "\/" (v102 "\/" v2)) "\/" (((v1 "\/" (v102 "\/" v2)) "/\" v101) "\/" v102) = v1 "\/" (v102 "\/" v2) by A25; :: thesis: verum

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

A89: for v101, v100, v0 being Element of L holds (v100 "\/" v101) "\/" (v101 "\/" (v0 "/\" v100)) = v100 "\/" v101

proof

let v101, v100, v0 be Element of L; :: thesis: (v100 "\/" v101) "\/" (v101 "\/" (v0 "/\" v100)) = v100 "\/" v101
(v0 "/\" v100) "/\" (v100 "\/" v101) = v0 "/\" v100 by A73;
hence (v100 "\/" v101) "\/" (v101 "\/" (v0 "/\" v100)) = v100 "\/" v101 by A41; :: thesis: verum

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

A104: 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 A101; :: thesis: verum

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

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

end;

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

end;

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

proof

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

end;

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

end;

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