let L be non empty LattStr ; :: thesis: ( L is satisfying_McKenzie_1 & L is satisfying_McKenzie_2 & ( for v2, v1, v0 being Element of L holds ((v0 "/\" v1) "\/" (v1 "/\" v2)) "\/" v1 = v1 ) & ( for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" (v1 "\/" v2)) "/\" v1 = v1 ) implies ( ( for v1, v0 being Element of L holds v0 "/\" (v0 "\/" v1) = v0 ) & ( for v1, v0 being Element of L holds v0 "\/" (v0 "/\" v1) = v0 ) & L is join-commutative & L is meet-commutative & L is meet-associative & L is join-associative ) )
assume A2: L is satisfying_McKenzie_1 ; :: thesis: ( not L is satisfying_McKenzie_2 or ex v2, v1, v0 being Element of L st not ((v0 "/\" v1) "\/" (v1 "/\" v2)) "\/" v1 = v1 or ex v2, v1, v0 being Element of L st not ((v0 "\/" v1) "/\" (v1 "\/" v2)) "/\" v1 = v1 or ( ( for v1, v0 being Element of L holds v0 "/\" (v0 "\/" v1) = v0 ) & ( for v1, v0 being Element of L holds v0 "\/" (v0 "/\" v1) = v0 ) & L is join-commutative & L is meet-commutative & L is meet-associative & L is join-associative ) )
assume A3: L is satisfying_McKenzie_2 ; :: thesis: ( ex v2, v1, v0 being Element of L st not ((v0 "/\" v1) "\/" (v1 "/\" v2)) "\/" v1 = v1 or ex v2, v1, v0 being Element of L st not ((v0 "\/" v1) "/\" (v1 "\/" v2)) "/\" v1 = v1 or ( ( for v1, v0 being Element of L holds v0 "/\" (v0 "\/" v1) = v0 ) & ( for v1, v0 being Element of L holds v0 "\/" (v0 "/\" v1) = v0 ) & L is join-commutative & L is meet-commutative & L is meet-associative & L is join-associative ) )
assume A4: for v2, v1, v0 being Element of L holds ((v0 "/\" v1) "\/" (v1 "/\" v2)) "\/" v1 = v1 ; :: thesis: ( ex v2, v1, v0 being Element of L st not ((v0 "\/" v1) "/\" (v1 "\/" v2)) "/\" v1 = v1 or ( ( for v1, v0 being Element of L holds v0 "/\" (v0 "\/" v1) = v0 ) & ( for v1, v0 being Element of L holds v0 "\/" (v0 "/\" v1) = v0 ) & L is join-commutative & L is meet-commutative & L is meet-associative & L is join-associative ) )
assume A5: for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" (v1 "\/" v2)) "/\" v1 = v1 ; :: thesis: ( ( for v1, v0 being Element of L holds v0 "/\" (v0 "\/" v1) = v0 ) & ( for v1, v0 being Element of L holds v0 "\/" (v0 "/\" v1) = v0 ) & L is join-commutative & L is meet-commutative & L is meet-associative & L is join-associative )
A9: for v100, v101 being Element of L holds v100 "\/" (v101 "/\" v100) = v100

proof

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

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

end;

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

end;

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

proof

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

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

end;

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

end;

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

proof

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

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

end;

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

end;

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

proof

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

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

end;

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

end;

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

proof

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

end;

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

proof

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

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

end;

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

end;

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

proof

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

end;

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

proof

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

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

end;

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

A65: 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 A21;
hence (v101 "\/" v1) "\/" v101 = v101 "\/" v1 by A9; :: thesis: verum

end;

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

proof

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

end;

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

A94: 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 "\/" (v0 "/\" v1) = v0 by A33;
hence (v0 "/\" v1) "\/" v0 = v0 by A91; :: thesis: verum

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

A143: 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 "/\" v100) "\/" v102 = v102 by A94;
hence (v100 "/\" v102) "/\" (v102 "/\" v100) = v102 "/\" v100 by A49; :: thesis: verum

end;

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

proof

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

end;

A151: 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 "\/" v100) "/\" v102 = v102 by A101;
hence (v100 "\/" v102) "\/" (v102 "\/" v100) = v102 "\/" v100 by A53; :: thesis: verum

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

A173: 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 A167;
hence v0 "/\" v1 = v1 "/\" v0 by A170; :: thesis: verum

end;

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

proof

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

end;

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

end;

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

end;

A191: 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 A151;
hence v0 "\/" v1 = v1 "\/" v0 by A188; :: thesis: verum

end;

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

proof

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

end;

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

end;

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

proof

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

end;

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

end;

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

proof

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

end;

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

end;

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

end;

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

proof

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

end;

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

end;

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

proof

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

end;

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

end;

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

proof

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

end;

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

proof

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

end;

A299: 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 A9;
hence (v1 "/\" v101) "/\" (v101 "/\" v102) = (v1 "/\" v101) "/\" v102 by A290; :: thesis: verum

end;

A303: 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 A33;
hence (v101 "/\" v1) "/\" (v101 "/\" v102) = (v101 "/\" v1) "/\" v102 by A290; :: thesis: verum

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

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

end;

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

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

end;

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

end;

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

proof

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

end;

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

proof

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

end;

hence ( ( for v1, v0 being Element of L holds v0 "/\" (v0 "\/" v1) = v0 ) & ( for v1, v0 being Element of L holds v0 "\/" (v0 "/\" v1) = v0 ) & L is join-commutative & L is meet-commutative & L is meet-associative & L is join-associative ) by A173, A191, A21, A33, A246; :: thesis: verum