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 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;

A16: 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;

A24: 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;

A28: 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;

A32: 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;

A42: 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 A28; :: thesis: verum

end;

A45: 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 A32;
hence (((v101 "/\" v1) "\/" v101) "/\" v101) "\/" (((v101 "/\" v1) "\/" v101) "/\" v101) = (v101 "/\" v1) "\/" v101 by A1; :: thesis: verum

end;

A49: 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 A28;
hence (v101 "\/" ((v101 "\/" v1) "/\" v101)) "\/" ((v101 "\/" v1) "/\" v101) = (v101 "\/" v1) "/\" v101 by A32; :: thesis: verum

end;

A60: for v0 being Element of L holds v0 "/\" v0 = v0 by A1, A4, A5, Lemma1;
A63: 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 A42;
hence ((v0 "/\" v1) "\/" (v0 "/\" (v0 "/\" v1))) "\/" (v0 "/\" (v0 "/\" v1)) = v0 "/\" (v0 "/\" v1) by A32; :: thesis: verum

end;

A75: 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 A60;
hence v0 "\/" (v1 "/\" (v0 "\/" v0)) = v0 by A2; :: thesis: verum

end;

A83: for v0 being Element of L holds v0 = v0 "\/" v0 by A1, A2, A3, A4, A5, Lemma2;
A86: 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 A83;
hence v0 "\/" (v1 "/\" v0) = v0 by A75; :: thesis: verum

end;

A88: 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 A83;
hence ((v0 "/\" v1) "\/" v0) "/\" v0 = (v0 "/\" v1) "\/" v0 by A45; :: thesis: verum

end;

A90: 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 A86;
hence (v0 "/\" v1) "\/" (v0 "/\" (v0 "/\" v1)) = v0 "/\" (v0 "/\" v1) by A63; :: thesis: verum

end;

A92: 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 A86;
hence v0 "/\" v1 = v0 "/\" (v0 "/\" v1) by A90; :: thesis: verum

end;

A95: 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 A86;
hence v0 "\/" ((v0 "\/" v1) "/\" v0) = (v0 "\/" v1) "/\" v0 by A49; :: thesis: verum

end;

A97: 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 A86;
hence v0 = (v0 "\/" v1) "/\" v0 by A95; :: thesis: verum

end;

A101: 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 A83;
hence (v101 "/\" (v102 "\/" v101)) "/\" v101 = v101 by A4; :: thesis: verum

end;

A105: 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 A32;
hence v101 "/\" ((v101 "/\" v1) "\/" v101) = (v101 "/\" v1) "\/" v101 by A97; :: thesis: verum

end;

A109: 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 A92;
hence (v100 "/\" v1) "\/" (v100 "/\" (v100 "\/" (v100 "/\" v1))) = v100 by A1; :: thesis: verum

end;

A113: 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 A92;
hence ((v100 "/\" v1) "/\" (v100 "/\" (v100 "\/" (v100 "/\" v1)))) "\/" ((v100 "/\" (v100 "/\" v1)) "/\" v100) = v100 "/\" (v100 "/\" v1) by A9; :: thesis: verum

end;

A116: 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 A92;
hence ((v0 "/\" v1) "/\" (v0 "/\" (v0 "\/" (v0 "/\" v1)))) "\/" ((v0 "/\" v1) "/\" v0) = v0 "/\" (v0 "/\" v1) by A113; :: thesis: verum

end;

A118: 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 A92;
hence ((v0 "/\" v1) "/\" (v0 "/\" (v0 "\/" (v0 "/\" v1)))) "\/" ((v0 "/\" v1) "/\" v0) = v0 "/\" v1 by A116; :: thesis: verum

end;

A121: 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 A32;
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 A12; :: thesis: verum

end;

A124: 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 A32;
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 A121; :: thesis: verum

end;

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

end;

A129: 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 A105;
hence ((v100 "/\" v1) "\/" v100) "/\" v100 = v100 by A101; :: thesis: verum

end;

A132: 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 A88;
hence (v0 "/\" v1) "\/" v0 = v0 by A129; :: thesis: verum

end;

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

end;

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

end;

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

end;

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

end;

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

end;

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

end;

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

end;

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

end;

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

end;

A154: 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 A132;
hence v0 = v0 "/\" (v1 "\/" v0) by A152; :: thesis: verum

end;

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

end;

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

end;

A161: 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 A157;
hence v0 "/\" (v0 "\/" (v0 "/\" v1)) = v0 by A109; :: thesis: verum

end;

A163: 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 A161;
hence ((v0 "/\" v1) "/\" v0) "\/" ((v0 "/\" v1) "/\" v0) = v0 "/\" v1 by A118; :: thesis: verum

end;

A165: 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 A83;
hence (v0 "/\" v1) "/\" v0 = v0 "/\" v1 by A163; :: thesis: verum

end;

A168: 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 A165;
hence v100 "\/" (v100 "/\" v1) = v100 by A86; :: thesis: verum

end;

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

proof

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

end;

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

proof

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

end;

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

proof

let v0, v1 be Element of L; :: thesis: v1 "/\" v0 = (v1 "/\" v0) "/\" (v0 "/\" v1)
(v0 "/\" v1) "/\" (v1 "/\" v0) = v1 "/\" v0 by A172;
hence v1 "/\" v0 = (v1 "/\" v0) "/\" (v0 "/\" v1) by A176; :: 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) = v1 "/\" v0 by A172;
hence v0 "/\" v1 = v1 "/\" v0 by A179; :: thesis: verum

end;

hence contradiction by A6; :: thesis: verum