let L be LATTICE; :: thesis:

now :: thesis:

given a, b, c, d, e being Element of L such that A1: b <> d and
A2: a "/\" b = a and
A3: d "/\" e = d and
A4: b "/\" d = b and
A5: c "/\" d = a and
A6: b "\/" c = 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; :: thesis:

end;

hence ( L is modular implies for a, b, c, d, e being Element of L holds
( not a,b,c,d,e are_mutually_distinct 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 :: thesis:

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

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,c,d,e are_mutually_distinct & 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

take y "/\" z ; :: thesis:
take x "\/" (y "/\" z) ; :: thesis:
take y ; :: thesis:
take (x "\/" y) "/\" z ; :: thesis:
take x "\/" y ; :: thesis:
A18: y <= x "\/" y by YELLOW_0:22;

now :: thesis:

A19: y "/\" z <= y by YELLOW_0:23;
assume A20: y "/\" z = x "\/" (y "/\" z) ; :: 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 y "/\" z <> x "\/" (y "/\" z) ; :: according to ZFMISC_1:def 7 :: thesis:

now :: thesis:

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

end;

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

now :: thesis:

assume y "/\" z = (x "\/" y) "/\" z ; :: 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 y "/\" z <> (x "\/" y) "/\" z ; :: thesis:
thus y "/\" z <> x "\/" y by A14; :: thesis:

now :: thesis:

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

end;

hence x "\/" (y "/\" z) <> y ; :: thesis:
thus x "\/" (y "/\" z) <> (x "\/" y) "/\" z by A9; :: thesis:

now :: thesis:

assume x "\/" y = x "\/" (y "/\" z) ; :: 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 x "\/" (y "/\" z) <> x "\/" y ; :: thesis:

now :: thesis:

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

end;

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

now :: thesis:

assume A30: y = x "\/" y ; :: 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 y <> x "\/" y ; :: thesis:

now :: thesis:

A31: y <= x "\/" y by YELLOW_0:22;
assume A32: (x "\/" y) "/\" z = x "\/" y ; :: 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 (x "\/" y) "/\" z <> x "\/" y ; :: thesis:
y "/\" z <= x "\/" (y "/\" z) by YELLOW_0:22;
hence (y "/\" z) "/\" (x "\/" (y "/\" z)) = y "/\" z by YELLOW_5:10; :: thesis:
y "/\" z <= y by YELLOW_0:23;
hence (y "/\" z) "/\" y = y "/\" z by YELLOW_5:10; :: thesis:
y <= x "\/" y by YELLOW_0:22;
hence y "/\" (x "\/" y) = y by YELLOW_5:10; :: thesis:
(x "\/" y) "/\" z <= x "\/" y by YELLOW_0:23;
hence ((x "\/" y) "/\" z) "/\" (x "\/" y) = (x "\/" y) "/\" z by YELLOW_5:10; :: thesis:
thus (x "\/" (y "/\" z)) "/\" y = y "/\" z by A16, A13, YELLOW_0:def 3; :: thesis:
thus (x "\/" (y "/\" z)) "/\" ((x "\/" y) "/\" z) = x "\/" (y "/\" z) by A8, Th8, YELLOW_5:10; :: thesis:
thus y "/\" ((x "\/" y) "/\" z) = (y "/\" (x "\/" y)) "/\" z by LATTICE3:16
.= y "/\" z by LATTICE3:18 ; :: thesis:
thus (x "\/" (y "/\" z)) "\/" y = x "\/" ((y "/\" z) "\/" y) by LATTICE3:14
.= x "\/" y 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 <= ((x "\/" y) "/\" z) "\/" y by YELLOW_5:7;
(x "\/" y) "/\" z <= x "\/" y by YELLOW_0:23;
then y "\/" ((x "\/" y) "/\" z) <= x "\/" y by A18, YELLOW_5:9;
hence y "\/" ((x "\/" y) "/\" z) = x "\/" y by A33, YELLOW_0:def 3; :: thesis:

end;

end;

hence ( ( for a, b, c, d, e being Element of L holds
( not a,b,c,d,e are_mutually_distinct 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: