let L be non empty LattStr ; :: thesis: ( ( for v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" (v0 "\/" v1)) = v0 ) & ( for v0, v1 being Element of L holds (v0 "/\" v0) "\/" (v1 "/\" (v0 "\/" v0)) = v0 ) & ( for v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1)) = v1 ) & ( for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" (v2 "\/" v0)) "/\" v0 = v0 ) & ( for v2, v1, v0 being Element of L holds ((v0 "/\" v1) "\/" (v2 "/\" v0)) "\/" v0 = v0 ) implies for v0, v1 being Element of L holds v0 "\/" v1 = v1 "\/" v0 )
assume A1: for v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" (v0 "\/" v1)) = v0 ; :: thesis: ( ex v0, v1 being Element of L st not (v0 "/\" v0) "\/" (v1 "/\" (v0 "\/" v0)) = v0 or ex v1, v0 being Element of L st not (v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1)) = v1 or ex v2, v1, v0 being Element of L st not ((v0 "\/" v1) "/\" (v2 "\/" v0)) "/\" v0 = v0 or ex v2, v1, v0 being Element of L st not ((v0 "/\" v1) "\/" (v2 "/\" v0)) "\/" v0 = v0 or for v0, v1 being Element of L holds v0 "\/" v1 = v1 "\/" v0 )
assume A2: for v0, v1 being Element of L holds (v0 "/\" v0) "\/" (v1 "/\" (v0 "\/" v0)) = v0 ; :: thesis: ( ex v1, v0 being Element of L st not (v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1)) = v1 or ex v2, v1, v0 being Element of L st not ((v0 "\/" v1) "/\" (v2 "\/" v0)) "/\" v0 = v0 or ex v2, v1, v0 being Element of L st not ((v0 "/\" v1) "\/" (v2 "/\" v0)) "\/" v0 = v0 or for v0, v1 being Element of L holds v0 "\/" v1 = v1 "\/" v0 )
assume A3: for v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1)) = v1 ; :: thesis: ( ex v2, v1, v0 being Element of L st not ((v0 "\/" v1) "/\" (v2 "\/" v0)) "/\" v0 = v0 or ex v2, v1, v0 being Element of L st not ((v0 "/\" v1) "\/" (v2 "/\" v0)) "\/" v0 = v0 or for v0, v1 being Element of L holds v0 "\/" v1 = v1 "\/" v0 )
assume A4: for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" (v2 "\/" v0)) "/\" v0 = v0 ; :: thesis: ( ex v2, v1, v0 being Element of L st not ((v0 "/\" v1) "\/" (v2 "/\" v0)) "\/" v0 = v0 or for v0, v1 being Element of L holds v0 "\/" v1 = v1 "\/" v0 )
assume A5: for v2, v1, v0 being Element of L holds ((v0 "/\" v1) "\/" (v2 "/\" v0)) "\/" v0 = v0 ; :: thesis: for v0, v1 being Element of L holds v0 "\/" v1 = v1 "\/" v0
assume not for v0, v1 being Element of L holds v0 "\/" v1 = v1 "\/" v0 ; :: thesis: contradiction
then consider C, D being Element of L such that
A6: C "\/" D <> D "\/" C ;
A9: for v1, v0 being Element of L holds ((v0 "/\" v1) "/\" (v0 "/\" (v0 "\/" v1))) "\/" ((v0 "/\" v1) "/\" v0) = v0 "/\" v1

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

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

end;

hence for v101, v100 being Element of L holds ((v100 "\/" v101) "/\" v100) "/\" v100 = v100 ; :: thesis: verum

end;

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

proof

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

end;

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

proof

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

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

end;

hence for v101, v100 being Element of L holds ((v100 "/\" v101) "\/" v100) "\/" v100 = v100 ; :: thesis: verum

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

A67: for v0 being Element of L holds v0 "/\" v0 = v0 by A1, A4, A5, Lemma1;
A70: for v1, v0 being Element of L holds ((v0 "/\" v1) "\/" (v0 "/\" (v0 "/\" v1))) "\/" (v0 "/\" (v0 "/\" v1)) = v0 "/\" (v0 "/\" v1)

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

A98: for v0 being Element of L holds v0 = v0 "\/" v0 by A1, A2, A3, A4, A5, Lemma2;
A101: for v0, v1 being Element of L holds v0 "\/" (v1 "/\" v0) = v0

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

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

end;

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

end;

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

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

A214: 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
(v0 "\/" v1) "/\" ((v0 "\/" v1) "\/" v0) = v0 "\/" v1 by A208;
hence (v0 "/\" (v0 "\/" v1)) "\/" (v0 "/\" (v0 "\/" v1)) = v0 by A135; :: thesis: verum

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

A227: 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 A216;
hence (v101 "\/" v1) "\/" v101 = v101 "\/" v1 by A101; :: thesis: verum

end;

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

proof

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

end;

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

proof

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

end;

A249: for v1, v0 being Element of L holds v0 "/\" v1 = v1 "/\" v0 by A1, A2, A3, A4, A5, Lemma3;
A251: for v2, v1, v0 being Element of L holds v1 "/\" ((v0 "\/" v1) "/\" (v1 "\/" v2)) = v1

proof

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

end;

A255: for v103, v100 being Element of L holds (v100 "\/" v103) "\/" ((v100 "\/" v103) "/\" (v103 "\/" v100)) = (v100 "\/" v103) "/\" (v103 "\/" v100)

proof

let v103, v100 be Element of L; :: thesis: (v100 "\/" v103) "\/" ((v100 "\/" v103) "/\" (v103 "\/" v100)) = (v100 "\/" v103) "/\" (v103 "\/" v100)
v103 "/\" ((v100 "\/" v103) "/\" (v103 "\/" v100)) = v103 by A251;
hence (v100 "\/" v103) "\/" ((v100 "\/" v103) "/\" (v103 "\/" v100)) = (v100 "\/" v103) "/\" (v103 "\/" v100) by A35; :: thesis: verum

end;

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

proof

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

end;

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

proof

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

end;

A266: 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
(v0 "\/" v1) "/\" (v1 "\/" v0) = v0 "\/" v1 by A258;
hence (v0 "\/" v1) "\/" (v1 "\/" v0) = v1 "\/" v0 by A141; :: thesis: verum

end;

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

proof

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

end;

hence contradiction by A6; :: thesis: verum