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

end;

assume A9: for v2, v1, v0 being Element of L holds ((v0 "/\" v1) "\/" (v2 "/\" v1)) "\/" v1 = v1 ; :: thesis: ( ex v1, v0 being Element of L st not v0 "/\" (v0 "\/" v1) = v0 or ex v0, v2, v1 being Element of L st not v0 "\/" (v1 "/\" v2) = (v0 "\/" v1) "/\" (v0 "\/" v2) or for v0, v1, v2 being Element of L holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) )
A11: 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 A4;
hence v1 "\/" ((v0 "/\" v1) "\/" (v2 "/\" v1)) = v1 by A9; :: thesis: verum

end;

assume A13: for v1, v0 being Element of L holds v0 "/\" (v0 "\/" v1) = v0 ; :: thesis: ( ex v0, v2, v1 being Element of L st not v0 "\/" (v1 "/\" v2) = (v0 "\/" v1) "/\" (v0 "\/" v2) or for v0, v1, v2 being Element of L holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) )
assume A15: for v0, v2, v1 being Element of L holds v0 "\/" (v1 "/\" v2) = (v0 "\/" v1) "/\" (v0 "\/" v2) ; :: thesis: for v0, v1, v2 being Element of L holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2)
A22: 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 A1;
hence v100 "/\" (v102 "\/" v100) = v100 by A7; :: thesis: verum

end;

A26: 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 A3;
hence v100 "\/" (v102 "/\" v100) = v100 by A11; :: thesis: verum

end;

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

proof

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

end;

A36: 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 A13;
hence (v101 "\/" v1) "\/" v101 = v101 "\/" v1 by A26; :: thesis: verum

end;

A39: 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 A4;
hence v0 "\/" (v0 "\/" v1) = v0 "\/" v1 by A36; :: thesis: verum

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

A89: 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 A86; :: thesis: verum

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

end;

A103: 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 A13;
hence (v101 "\/" v1) "\/" (v101 "\/" v102) = (v101 "\/" v1) "\/" v102 by A99; :: thesis: verum

end;

A107: 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 A22;
hence (v1 "\/" v101) "\/" (v101 "\/" v102) = (v1 "\/" v101) "\/" v102 by A99; :: thesis: verum

end;

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

end;

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

end;

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