let L be LATTICE; :: thesis:

given a, b, c, d, e being Element of L such that a <> b and
a <> c and
a <> d and
a <> e and
b <> c and
A1: b <> d and
b <> e and
c <> d and
c <> e and
d <> e and
A2: a "/\" b = a and
a "/\" c = a and
c "/\" e = c and
A3: d "/\" e = d and
b "/\" c = a and
A4: b "/\" d = b and
A5: c "/\" d = a and
A6: b "\/" c = e and
c "\/" d = e ; :: thesis:
A7: b <= d by A4, YELLOW_0:23;
b "\/" (c "/\" d) = b by A2, A5, Th5;
hence not L is modular by A1, A3, A6, A7, Def3; :: thesis:

end;

hence ( L is modular implies for a, b, c, d, e being Element of L holds
( not a <> b or not a <> c or not a <> d or not a <> e or not b <> c or not b <> d or not b <> e or not c <> d or not c <> e or not d <> e or not a "/\" b = a or not a "/\" c = a or not c "/\" e = c or not d "/\" e = d or not b "/\" c = a or not b "/\" d = b or not c "/\" d = a or not b "\/" c = e or not c "\/" d = e ) ) ; :: thesis:

now

assume not L is modular ; :: thesis:
then consider x, y, z being Element of L such that
A8: x <= z and
A9: x "\/" (y "/\" z) <> (x "\/" y) "/\" z by Def3;
x "\/" (y "/\" z) <= z "\/" (y "/\" z) by A8, YELLOW_5:7;
then A10: x "\/" (y "/\" z) <= z by LATTICE3:17;
set z1 = (x "\/" y) "/\" z;
set y1 = y;
x "\/" y <= x "\/" y ;
then (x "\/" y) "/\" x <= (x "\/" y) "/\" z by A8, YELLOW_3:2;
then x <= (x "\/" y) "/\" z by LATTICE3:18;
then A11: x "\/" y <= ((x "\/" y) "/\" z) "\/" y by YELLOW_5:7;
set x1 = x "\/" (y "/\" z);
A12: y "/\" z <= y by YELLOW_0:23;
y <= y ;
then A13: (x "\/" (y "/\" z)) "/\" y <= y "/\" z by A10, YELLOW_3:2;
set t = x "\/" y;
set b = y "/\" z;

A14: now

assume A15: y "/\" z = x "\/" y ; :: thesis:
then (x "\/" y) "/\" z = y "/\" (z "/\" z) by LATTICE3:16
.= x "\/" y by A15, YELLOW_5:2
.= (x "\/" x) "\/" y by YELLOW_5:1
.= x "\/" (y "/\" z) by A15, LATTICE3:14 ;
hence contradiction by A9; :: thesis:

end;

y "/\" z <= x "\/" (y "/\" z) by YELLOW_0:22;
then (y "/\" z) "/\" (y "/\" z) <= (x "\/" (y "/\" z)) "/\" y by A12, YELLOW_3:2;
then A16: y "/\" z <= (x "\/" (y "/\" z)) "/\" y by YELLOW_5:2;
A17: (x "\/" y) "/\" z <= x "\/" y by YELLOW_0:23;
thus ex a, b, c, d, e being Element of L st
( a <> b & a <> c & a <> d & a <> e & b <> c & b <> d & b <> e & c <> d & c <> e & d <> e & a "/\" b = a & a "/\" c = a & c "/\" e = c & d "/\" e = d & b "/\" c = a & b "/\" d = b & c "/\" d = a & b "\/" c = e & c "\/" d = e ) :: thesis:

proof

reconsider b = y "/\" z, x1 = x "\/" (y "/\" z), y1 = y, z1 = (x "\/" y) "/\" z, t = x "\/" y as Element of L ;
take b ; :: thesis:
take x1 ; :: thesis:
take y1 ; :: thesis:
take z1 ; :: thesis:
take t ; :: thesis:
A18: y1 <= x "\/" y by YELLOW_0:22;

now

A19: y "/\" z <= y by YELLOW_0:23;
assume A20: b = x1 ; :: thesis:
then x <= y "/\" z by YELLOW_0:22;
then x <= y by A19, YELLOW_0:def 2;
hence contradiction by A9, A20, YELLOW_5:8; :: thesis:

end;

hence b <> x1 ; :: thesis:

now

assume A21: b = y1 ; :: thesis:
then y <= z by YELLOW_0:23;
hence contradiction by A8, A9, A21, YELLOW_5:9, YELLOW_5:10; :: thesis:

end;

hence b <> y1 ; :: thesis:

now

assume b = z1 ; :: thesis:
then A22: (x "\/" y) "/\" z <= x "\/" (y "/\" z) by YELLOW_0:22;
x "\/" (y "/\" z) <= (x "\/" y) "/\" z by A8, Th8;
hence contradiction by A9, A22, YELLOW_0:def 3; :: thesis:

end;

hence b <> z1 ; :: thesis:
thus b <> t by A14; :: thesis:

now

A23: x1 "\/" y1 = x "\/" ((y "/\" z) "\/" y) by LATTICE3:14
.= t by LATTICE3:17 ;
assume A24: x1 = y1 ; :: thesis:
then A25: x1 "\/" y1 = x1 by YELLOW_5:1;
x1 "/\" y1 = x1 by A24, YELLOW_5:2;
hence contradiction by A16, A13, A14, A25, A23, YELLOW_0:def 3; :: thesis:

end;

hence x1 <> y1 ; :: thesis:
thus x1 <> z1 by A9; :: thesis:

now

assume t = x1 ; :: thesis:
then A26: (x "\/" y) "/\" z <= x "\/" (y "/\" z) by YELLOW_0:23;
x "\/" (y "/\" z) <= (x "\/" y) "/\" z by A8, Th8;
hence contradiction by A9, A26, YELLOW_0:def 3; :: thesis:

end;

hence x1 <> t ; :: thesis:

now

A27: y1 "/\" z1 = ((x "\/" y) "/\" y) "/\" z by LATTICE3:16
.= b by LATTICE3:18 ;
assume A28: y1 = z1 ; :: thesis:
then A29: z1 "\/" y1 = z1 by YELLOW_5:1;
z1 "/\" y1 = z1 by A28, YELLOW_5:2;
hence contradiction by A14, A17, A11, A29, A27, YELLOW_0:def 3; :: thesis:

end;

hence y1 <> z1 ; :: thesis:

now

assume A30: y1 = t ; :: thesis:
then x <= y by YELLOW_0:22;
then x "/\" x <= y "/\" z by A8, YELLOW_3:2;
then x <= y "/\" z by YELLOW_5:2;
hence contradiction by A9, A30, YELLOW_5:8; :: thesis:

end;

hence y1 <> t ; :: thesis:

now

A31: y <= x "\/" y by YELLOW_0:22;
assume A32: z1 = t ; :: thesis:
then x "\/" y <= z by YELLOW_0:23;
then y <= z by A31, YELLOW_0:def 2;
hence contradiction by A9, A32, YELLOW_5:10; :: thesis:

end;

hence z1 <> t ; :: thesis:
b <= x1 by YELLOW_0:22;
hence b "/\" x1 = b by YELLOW_5:10; :: thesis:
b <= y1 by YELLOW_0:23;
hence b "/\" y1 = b by YELLOW_5:10; :: thesis:
y1 <= t by YELLOW_0:22;
hence y1 "/\" t = y1 by YELLOW_5:10; :: thesis:
z1 <= t by YELLOW_0:23;
hence z1 "/\" t = z1 by YELLOW_5:10; :: thesis:
thus x1 "/\" y1 = b by A16, A13, YELLOW_0:def 3; :: thesis:
thus x1 "/\" z1 = x1 by A8, Th8, YELLOW_5:10; :: thesis:
thus y1 "/\" z1 = (y "/\" (x "\/" y)) "/\" z by LATTICE3:16
.= b by LATTICE3:18 ; :: thesis:
thus x1 "\/" y1 = x "\/" ((y "/\" z) "\/" y) by LATTICE3:14
.= t by LATTICE3:17 ; :: thesis:
x "\/" y <= x "\/" y ;
then (x "\/" y) "/\" x <= (x "\/" y) "/\" z by A8, YELLOW_3:2;
then x <= (x "\/" y) "/\" z by LATTICE3:18;
then A33: x "\/" y <= z1 "\/" y1 by YELLOW_5:7;
z1 <= x "\/" y by YELLOW_0:23;
then y1 "\/" z1 <= x "\/" y by A18, YELLOW_5:9;
hence y1 "\/" z1 = t by A33, YELLOW_0:def 3; :: thesis:

end;

hence ( ( for a, b, c, d, e being Element of L holds
( not a <> b or not a <> c or not a <> d or not a <> e or not b <> c or not b <> d or not b <> e or not c <> d or not c <> e or not d <> e or not a "/\" b = a or not a "/\" c = a or not c "/\" e = c or not d "/\" e = d or not b "/\" c = a or not b "/\" d = b or not c "/\" d = a or not b "\/" c = e or not c "\/" d = e ) ) implies L is modular ) ; :: thesis: