let L be LATTICE; :: thesis:
thus ( 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:

proof

now

given a, b, c, d, e being Element of L such that A1: ( a <> b & a <> c & a <> d & a <> e & b <> c & b <> d & b <> e & c <> d & c <> e & d <> e ) and
A2: ( 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:
A3: b "\/" (c "/\" d) = b by A2, Th5;
b <= d by A2, YELLOW_0:23;
hence not L is modular by A1, A2, A3, 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:

end;

now

assume not L is modular ; :: thesis:
then consider x, y, z being Element of L such that
A4: ( x <= z & x "\/" (y "/\" z) <> (x "\/" y) "/\" z ) by Def3;
set b = y "/\" z;
set x1 = x "\/" (y "/\" z);
set y1 = y;
set z1 = (x "\/" y) "/\" z;
set t = x "\/" y;
( y "/\" z <= x "\/" (y "/\" z) & y "/\" z <= y ) by YELLOW_0:22, YELLOW_0:23;
then (y "/\" z) "/\" (y "/\" z) <= (x "\/" (y "/\" z)) "/\" y by YELLOW_3:2;
then A5: y "/\" z <= (x "\/" (y "/\" z)) "/\" y by YELLOW_5:2;
x "\/" (y "/\" z) <= z "\/" (y "/\" z) by A4, YELLOW_5:7;
then ( x "\/" (y "/\" z) <= z & y <= y ) by LATTICE3:17;
then A6: (x "\/" (y "/\" z)) "/\" y <= y "/\" z by YELLOW_3:2;
A7: y "/\" z <> x "\/" y

proof

now

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

end;

hence y "/\" z <> x "\/" y ; :: thesis:

end;

A9: ( (x "\/" y) "/\" z <= x "\/" y & y <= x "\/" y ) by YELLOW_0:22, YELLOW_0:23;
( x <= z & x "\/" y <= x "\/" y ) by A4;
then (x "\/" y) "/\" x <= (x "\/" y) "/\" z by YELLOW_3:2;
then x <= (x "\/" y) "/\" z by LATTICE3:18;
then A10: x "\/" y <= ((x "\/" y) "/\" z) "\/" y by YELLOW_5:7;
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:
thus b <> x1 :: thesis:

proof

now

assume A11: b = x1 ; :: thesis:
then ( x <= y "/\" z & y "/\" z <= y ) by YELLOW_0:22, YELLOW_0:23;
then x <= y by YELLOW_0:def 2;
hence contradiction by A4, A11, YELLOW_5:8; :: thesis:

end;

hence b <> x1 ; :: thesis:

end;

thus b <> y1 :: thesis:

proof

now

assume A12: b = y1 ; :: thesis:
then ( x <= z & y <= z ) by A4, YELLOW_0:23;
hence contradiction by A4, A12, YELLOW_5:9, YELLOW_5:10; :: thesis:

end;

hence b <> y1 ; :: thesis:

end;

thus b <> z1 :: thesis:

proof

now

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

end;

hence b <> z1 ; :: thesis:

end;

thus b <> t by A7; :: thesis:
thus x1 <> y1 :: thesis:

proof

now

assume x1 = y1 ; :: thesis:
then A14: ( x1 "/\" y1 = x1 & x1 "\/" y1 = x1 ) by YELLOW_5:1, YELLOW_5:2;
x1 "\/" y1 = x "\/" ((y "/\" z) "\/" y) by LATTICE3:14
.= t by LATTICE3:17 ;
hence contradiction by A5, A6, A7, A14, YELLOW_0:def 3; :: thesis:

end;

hence x1 <> y1 ; :: thesis:

end;

thus x1 <> z1 by A4; :: thesis:
thus x1 <> t :: thesis:

proof

now

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

end;

hence x1 <> t ; :: thesis:

end;

thus y1 <> z1 :: thesis:

proof

now

assume y1 = z1 ; :: thesis:
then A16: ( z1 "/\" y1 = z1 & z1 "\/" y1 = z1 ) by YELLOW_5:1, YELLOW_5:2;
y1 "/\" z1 = ((x "\/" y) "/\" y) "/\" z by LATTICE3:16
.= b by LATTICE3:18 ;
hence contradiction by A7, A9, A10, A16, YELLOW_0:def 3; :: thesis:

end;

hence y1 <> z1 ; :: thesis:

end;

thus y1 <> t :: thesis:

proof

now

assume A17: y1 = t ; :: thesis:
then ( x <= z & x <= y ) by A4, YELLOW_0:22;
then x "/\" x <= y "/\" z by YELLOW_3:2;
then x <= y "/\" z by YELLOW_5:2;
hence contradiction by A4, A17, YELLOW_5:8; :: thesis:

end;

hence y1 <> t ; :: thesis:

end;

thus z1 <> t :: thesis:

proof

now

assume A18: z1 = t ; :: thesis:
then ( y <= x "\/" y & x "\/" y <= z ) by YELLOW_0:22, YELLOW_0:23;
then y <= z by YELLOW_0:def 2;
hence contradiction by A4, A18, YELLOW_5:10; :: thesis:

end;

hence z1 <> t ; :: thesis:

end;

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 A5, A6, YELLOW_0:def 3; :: thesis:
thus x1 "/\" z1 = x1 by A4, 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:
( z1 <= x "\/" y & y1 <= x "\/" y ) by YELLOW_0:22, YELLOW_0:23;
then A19: y1 "\/" z1 <= x "\/" y by YELLOW_5:9;
( x <= z & x "\/" y <= x "\/" y ) by A4;
then (x "\/" y) "/\" x <= (x "\/" y) "/\" z by YELLOW_3:2;
then x <= (x "\/" y) "/\" z by LATTICE3:18;
then x "\/" y <= z1 "\/" y1 by YELLOW_5:7;
hence y1 "\/" z1 = t by A19, 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: