let L be LATTICE; :: thesis: ( L is modular iff 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 ) )

( 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: ( ( 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 )

( 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: verum

( 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 ) )

now :: thesis: ( ex a, b, c, d, e being Element of L st

( b <> d & a "/\" b = a & d "/\" e = d & b "/\" d = b & c "/\" d = a & b "\/" c = e ) implies not L is modular )

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

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: not L is modular

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: verum

end;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: not L is modular

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: verum

( 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: ( ( 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 )

now :: thesis: ( not L is modular implies 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 ) )

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

assume
not L is modular
; :: thesis: 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 )

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;

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: verum

end;( 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 )

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: not y "/\" z = x "\/" y

y "/\" z <= x "\/" (y "/\" z)
by YELLOW_0:22;assume A15:
y "/\" z = x "\/" y
; :: thesis: contradiction

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: verum

end;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: verum

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: verum

proof

take
y "/\" z
; :: thesis: ex b, c, d, e being Element of L st

( y "/\" z,b,c,d,e are_mutually_distinct & (y "/\" z) "/\" b = y "/\" z & (y "/\" z) "/\" c = y "/\" z & c "/\" e = c & d "/\" e = d & b "/\" c = y "/\" z & b "/\" d = b & c "/\" d = y "/\" z & b "\/" c = e & c "\/" d = e )

take x "\/" (y "/\" z) ; :: thesis: ex c, d, e being Element of L st

( y "/\" z,x "\/" (y "/\" z),c,d,e are_mutually_distinct & (y "/\" z) "/\" (x "\/" (y "/\" z)) = y "/\" z & (y "/\" z) "/\" c = y "/\" z & c "/\" e = c & d "/\" e = d & (x "\/" (y "/\" z)) "/\" c = y "/\" z & (x "\/" (y "/\" z)) "/\" d = x "\/" (y "/\" z) & c "/\" d = y "/\" z & (x "\/" (y "/\" z)) "\/" c = e & c "\/" d = e )

take y ; :: thesis: ex d, e being Element of L st

( y "/\" z,x "\/" (y "/\" z),y,d,e are_mutually_distinct & (y "/\" z) "/\" (x "\/" (y "/\" z)) = y "/\" z & (y "/\" z) "/\" y = y "/\" z & y "/\" e = y & d "/\" e = d & (x "\/" (y "/\" z)) "/\" y = y "/\" z & (x "\/" (y "/\" z)) "/\" d = x "\/" (y "/\" z) & y "/\" d = y "/\" z & (x "\/" (y "/\" z)) "\/" y = e & y "\/" d = e )

take (x "\/" y) "/\" z ; :: thesis: ex e being Element of L st

( y "/\" z,x "\/" (y "/\" z),y,(x "\/" y) "/\" z,e are_mutually_distinct & (y "/\" z) "/\" (x "\/" (y "/\" z)) = y "/\" z & (y "/\" z) "/\" y = y "/\" z & y "/\" e = y & ((x "\/" y) "/\" z) "/\" e = (x "\/" y) "/\" z & (x "\/" (y "/\" z)) "/\" y = y "/\" z & (x "\/" (y "/\" z)) "/\" ((x "\/" y) "/\" z) = x "\/" (y "/\" z) & y "/\" ((x "\/" y) "/\" z) = y "/\" z & (x "\/" (y "/\" z)) "\/" y = e & y "\/" ((x "\/" y) "/\" z) = e )

take x "\/" y ; :: thesis: ( y "/\" z,x "\/" (y "/\" z),y,(x "\/" y) "/\" z,x "\/" y are_mutually_distinct & (y "/\" z) "/\" (x "\/" (y "/\" z)) = y "/\" z & (y "/\" z) "/\" y = y "/\" z & y "/\" (x "\/" y) = y & ((x "\/" y) "/\" z) "/\" (x "\/" y) = (x "\/" y) "/\" z & (x "\/" (y "/\" z)) "/\" y = y "/\" z & (x "\/" (y "/\" z)) "/\" ((x "\/" y) "/\" z) = x "\/" (y "/\" z) & y "/\" ((x "\/" y) "/\" z) = y "/\" z & (x "\/" (y "/\" z)) "\/" y = x "\/" y & y "\/" ((x "\/" y) "/\" z) = x "\/" y )

A18: y <= x "\/" y by YELLOW_0:22;

thus y "/\" z <> x "\/" y by A14; :: thesis: ( not x "\/" (y "/\" z) = y & not x "\/" (y "/\" z) = (x "\/" y) "/\" z & not x "\/" (y "/\" z) = x "\/" y & not y = (x "\/" y) "/\" z & not y = x "\/" y & not (x "\/" y) "/\" z = x "\/" y & (y "/\" z) "/\" (x "\/" (y "/\" z)) = y "/\" z & (y "/\" z) "/\" y = y "/\" z & y "/\" (x "\/" y) = y & ((x "\/" y) "/\" z) "/\" (x "\/" y) = (x "\/" y) "/\" z & (x "\/" (y "/\" z)) "/\" y = y "/\" z & (x "\/" (y "/\" z)) "/\" ((x "\/" y) "/\" z) = x "\/" (y "/\" z) & y "/\" ((x "\/" y) "/\" z) = y "/\" z & (x "\/" (y "/\" z)) "\/" y = x "\/" y & y "\/" ((x "\/" y) "/\" z) = x "\/" y )

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

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 = y "/\" z & y "/\" (x "\/" y) = y & ((x "\/" y) "/\" z) "/\" (x "\/" y) = (x "\/" y) "/\" z & (x "\/" (y "/\" z)) "/\" y = y "/\" z & (x "\/" (y "/\" z)) "/\" ((x "\/" y) "/\" z) = x "\/" (y "/\" z) & y "/\" ((x "\/" y) "/\" z) = y "/\" z & (x "\/" (y "/\" z)) "\/" y = x "\/" y & y "\/" ((x "\/" y) "/\" z) = x "\/" y )

y "/\" z <= y by YELLOW_0:23;

hence (y "/\" z) "/\" y = y "/\" z by YELLOW_5:10; :: thesis: ( y "/\" (x "\/" y) = y & ((x "\/" y) "/\" z) "/\" (x "\/" y) = (x "\/" y) "/\" z & (x "\/" (y "/\" z)) "/\" y = y "/\" z & (x "\/" (y "/\" z)) "/\" ((x "\/" y) "/\" z) = x "\/" (y "/\" z) & y "/\" ((x "\/" y) "/\" z) = y "/\" z & (x "\/" (y "/\" z)) "\/" y = x "\/" y & y "\/" ((x "\/" y) "/\" z) = x "\/" y )

y <= x "\/" y by YELLOW_0:22;

hence y "/\" (x "\/" y) = y by YELLOW_5:10; :: thesis: ( ((x "\/" y) "/\" z) "/\" (x "\/" y) = (x "\/" y) "/\" z & (x "\/" (y "/\" z)) "/\" y = y "/\" z & (x "\/" (y "/\" z)) "/\" ((x "\/" y) "/\" z) = x "\/" (y "/\" z) & y "/\" ((x "\/" y) "/\" z) = y "/\" z & (x "\/" (y "/\" z)) "\/" y = x "\/" y & y "\/" ((x "\/" y) "/\" z) = x "\/" y )

(x "\/" y) "/\" z <= x "\/" y by YELLOW_0:23;

hence ((x "\/" y) "/\" z) "/\" (x "\/" y) = (x "\/" y) "/\" z by YELLOW_5:10; :: thesis: ( (x "\/" (y "/\" z)) "/\" y = y "/\" z & (x "\/" (y "/\" z)) "/\" ((x "\/" y) "/\" z) = x "\/" (y "/\" z) & y "/\" ((x "\/" y) "/\" z) = y "/\" z & (x "\/" (y "/\" z)) "\/" y = x "\/" y & y "\/" ((x "\/" y) "/\" z) = x "\/" y )

thus (x "\/" (y "/\" z)) "/\" y = y "/\" z by A16, A13, YELLOW_0:def 3; :: thesis: ( (x "\/" (y "/\" z)) "/\" ((x "\/" y) "/\" z) = x "\/" (y "/\" z) & y "/\" ((x "\/" y) "/\" z) = y "/\" z & (x "\/" (y "/\" z)) "\/" y = x "\/" y & y "\/" ((x "\/" y) "/\" z) = x "\/" y )

thus (x "\/" (y "/\" z)) "/\" ((x "\/" y) "/\" z) = x "\/" (y "/\" z) by A8, Th8, YELLOW_5:10; :: thesis: ( y "/\" ((x "\/" y) "/\" z) = y "/\" z & (x "\/" (y "/\" z)) "\/" y = x "\/" y & y "\/" ((x "\/" y) "/\" z) = x "\/" y )

thus y "/\" ((x "\/" y) "/\" z) = (y "/\" (x "\/" y)) "/\" z by LATTICE3:16

.= y "/\" z by LATTICE3:18 ; :: thesis: ( (x "\/" (y "/\" z)) "\/" y = x "\/" y & y "\/" ((x "\/" y) "/\" z) = x "\/" y )

thus (x "\/" (y "/\" z)) "\/" y = x "\/" ((y "/\" z) "\/" y) by LATTICE3:14

.= x "\/" y by LATTICE3:17 ; :: thesis: y "\/" ((x "\/" y) "/\" z) = x "\/" 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 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: verum

end;( y "/\" z,b,c,d,e are_mutually_distinct & (y "/\" z) "/\" b = y "/\" z & (y "/\" z) "/\" c = y "/\" z & c "/\" e = c & d "/\" e = d & b "/\" c = y "/\" z & b "/\" d = b & c "/\" d = y "/\" z & b "\/" c = e & c "\/" d = e )

take x "\/" (y "/\" z) ; :: thesis: ex c, d, e being Element of L st

( y "/\" z,x "\/" (y "/\" z),c,d,e are_mutually_distinct & (y "/\" z) "/\" (x "\/" (y "/\" z)) = y "/\" z & (y "/\" z) "/\" c = y "/\" z & c "/\" e = c & d "/\" e = d & (x "\/" (y "/\" z)) "/\" c = y "/\" z & (x "\/" (y "/\" z)) "/\" d = x "\/" (y "/\" z) & c "/\" d = y "/\" z & (x "\/" (y "/\" z)) "\/" c = e & c "\/" d = e )

take y ; :: thesis: ex d, e being Element of L st

( y "/\" z,x "\/" (y "/\" z),y,d,e are_mutually_distinct & (y "/\" z) "/\" (x "\/" (y "/\" z)) = y "/\" z & (y "/\" z) "/\" y = y "/\" z & y "/\" e = y & d "/\" e = d & (x "\/" (y "/\" z)) "/\" y = y "/\" z & (x "\/" (y "/\" z)) "/\" d = x "\/" (y "/\" z) & y "/\" d = y "/\" z & (x "\/" (y "/\" z)) "\/" y = e & y "\/" d = e )

take (x "\/" y) "/\" z ; :: thesis: ex e being Element of L st

( y "/\" z,x "\/" (y "/\" z),y,(x "\/" y) "/\" z,e are_mutually_distinct & (y "/\" z) "/\" (x "\/" (y "/\" z)) = y "/\" z & (y "/\" z) "/\" y = y "/\" z & y "/\" e = y & ((x "\/" y) "/\" z) "/\" e = (x "\/" y) "/\" z & (x "\/" (y "/\" z)) "/\" y = y "/\" z & (x "\/" (y "/\" z)) "/\" ((x "\/" y) "/\" z) = x "\/" (y "/\" z) & y "/\" ((x "\/" y) "/\" z) = y "/\" z & (x "\/" (y "/\" z)) "\/" y = e & y "\/" ((x "\/" y) "/\" z) = e )

take x "\/" y ; :: thesis: ( y "/\" z,x "\/" (y "/\" z),y,(x "\/" y) "/\" z,x "\/" y are_mutually_distinct & (y "/\" z) "/\" (x "\/" (y "/\" z)) = y "/\" z & (y "/\" z) "/\" y = y "/\" z & y "/\" (x "\/" y) = y & ((x "\/" y) "/\" z) "/\" (x "\/" y) = (x "\/" y) "/\" z & (x "\/" (y "/\" z)) "/\" y = y "/\" z & (x "\/" (y "/\" z)) "/\" ((x "\/" y) "/\" z) = x "\/" (y "/\" z) & y "/\" ((x "\/" y) "/\" z) = y "/\" z & (x "\/" (y "/\" z)) "\/" y = x "\/" y & y "\/" ((x "\/" y) "/\" z) = x "\/" y )

A18: y <= x "\/" y by YELLOW_0:22;

now :: thesis: not y "/\" z = x "\/" (y "/\" z)

hence
y "/\" z <> x "\/" (y "/\" z)
; :: according to ZFMISC_1:def 7 :: thesis: ( not y "/\" z = y & not y "/\" z = (x "\/" y) "/\" z & not y "/\" z = x "\/" y & not x "\/" (y "/\" z) = y & not x "\/" (y "/\" z) = (x "\/" y) "/\" z & not x "\/" (y "/\" z) = x "\/" y & not y = (x "\/" y) "/\" z & not y = x "\/" y & not (x "\/" y) "/\" z = x "\/" y & (y "/\" z) "/\" (x "\/" (y "/\" z)) = y "/\" z & (y "/\" z) "/\" y = y "/\" z & y "/\" (x "\/" y) = y & ((x "\/" y) "/\" z) "/\" (x "\/" y) = (x "\/" y) "/\" z & (x "\/" (y "/\" z)) "/\" y = y "/\" z & (x "\/" (y "/\" z)) "/\" ((x "\/" y) "/\" z) = x "\/" (y "/\" z) & y "/\" ((x "\/" y) "/\" z) = y "/\" z & (x "\/" (y "/\" z)) "\/" y = x "\/" y & y "\/" ((x "\/" y) "/\" z) = x "\/" y )A19:
y "/\" z <= y
by YELLOW_0:23;

assume A20: y "/\" z = x "\/" (y "/\" z) ; :: thesis: contradiction

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: verum

end;assume A20: y "/\" z = x "\/" (y "/\" z) ; :: thesis: contradiction

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: verum

now :: thesis: not y "/\" z = y

hence
y "/\" z <> y
; :: thesis: ( not y "/\" z = (x "\/" y) "/\" z & not y "/\" z = x "\/" y & not x "\/" (y "/\" z) = y & not x "\/" (y "/\" z) = (x "\/" y) "/\" z & not x "\/" (y "/\" z) = x "\/" y & not y = (x "\/" y) "/\" z & not y = x "\/" y & not (x "\/" y) "/\" z = x "\/" y & (y "/\" z) "/\" (x "\/" (y "/\" z)) = y "/\" z & (y "/\" z) "/\" y = y "/\" z & y "/\" (x "\/" y) = y & ((x "\/" y) "/\" z) "/\" (x "\/" y) = (x "\/" y) "/\" z & (x "\/" (y "/\" z)) "/\" y = y "/\" z & (x "\/" (y "/\" z)) "/\" ((x "\/" y) "/\" z) = x "\/" (y "/\" z) & y "/\" ((x "\/" y) "/\" z) = y "/\" z & (x "\/" (y "/\" z)) "\/" y = x "\/" y & y "\/" ((x "\/" y) "/\" z) = x "\/" y )assume A21:
y "/\" z = y
; :: thesis: contradiction

then y <= z by YELLOW_0:23;

hence contradiction by A8, A9, A21, YELLOW_5:9, YELLOW_5:10; :: thesis: verum

end;then y <= z by YELLOW_0:23;

hence contradiction by A8, A9, A21, YELLOW_5:9, YELLOW_5:10; :: thesis: verum

now :: thesis: not y "/\" z = (x "\/" y) "/\" z

hence
y "/\" z <> (x "\/" y) "/\" z
; :: thesis: ( not y "/\" z = x "\/" y & not x "\/" (y "/\" z) = y & not x "\/" (y "/\" z) = (x "\/" y) "/\" z & not x "\/" (y "/\" z) = x "\/" y & not y = (x "\/" y) "/\" z & not y = x "\/" y & not (x "\/" y) "/\" z = x "\/" y & (y "/\" z) "/\" (x "\/" (y "/\" z)) = y "/\" z & (y "/\" z) "/\" y = y "/\" z & y "/\" (x "\/" y) = y & ((x "\/" y) "/\" z) "/\" (x "\/" y) = (x "\/" y) "/\" z & (x "\/" (y "/\" z)) "/\" y = y "/\" z & (x "\/" (y "/\" z)) "/\" ((x "\/" y) "/\" z) = x "\/" (y "/\" z) & y "/\" ((x "\/" y) "/\" z) = y "/\" z & (x "\/" (y "/\" z)) "\/" y = x "\/" y & y "\/" ((x "\/" y) "/\" z) = x "\/" y )assume
y "/\" z = (x "\/" y) "/\" z
; :: thesis: contradiction

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: verum

end;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: verum

thus y "/\" z <> x "\/" y by A14; :: thesis: ( not x "\/" (y "/\" z) = y & not x "\/" (y "/\" z) = (x "\/" y) "/\" z & not x "\/" (y "/\" z) = x "\/" y & not y = (x "\/" y) "/\" z & not y = x "\/" y & not (x "\/" y) "/\" z = x "\/" y & (y "/\" z) "/\" (x "\/" (y "/\" z)) = y "/\" z & (y "/\" z) "/\" y = y "/\" z & y "/\" (x "\/" y) = y & ((x "\/" y) "/\" z) "/\" (x "\/" y) = (x "\/" y) "/\" z & (x "\/" (y "/\" z)) "/\" y = y "/\" z & (x "\/" (y "/\" z)) "/\" ((x "\/" y) "/\" z) = x "\/" (y "/\" z) & y "/\" ((x "\/" y) "/\" z) = y "/\" z & (x "\/" (y "/\" z)) "\/" y = x "\/" y & y "\/" ((x "\/" y) "/\" z) = x "\/" y )

now :: thesis: not x "\/" (y "/\" z) = y

hence
x "\/" (y "/\" z) <> y
; :: thesis: ( not x "\/" (y "/\" z) = (x "\/" y) "/\" z & not x "\/" (y "/\" z) = x "\/" y & not y = (x "\/" y) "/\" z & not y = x "\/" y & not (x "\/" y) "/\" z = x "\/" y & (y "/\" z) "/\" (x "\/" (y "/\" z)) = y "/\" z & (y "/\" z) "/\" y = y "/\" z & y "/\" (x "\/" y) = y & ((x "\/" y) "/\" z) "/\" (x "\/" y) = (x "\/" y) "/\" z & (x "\/" (y "/\" z)) "/\" y = y "/\" z & (x "\/" (y "/\" z)) "/\" ((x "\/" y) "/\" z) = x "\/" (y "/\" z) & y "/\" ((x "\/" y) "/\" z) = y "/\" z & (x "\/" (y "/\" z)) "\/" y = x "\/" y & y "\/" ((x "\/" y) "/\" z) = x "\/" y )A23: (x "\/" (y "/\" z)) "\/" y =
x "\/" ((y "/\" z) "\/" y)
by LATTICE3:14

.= x "\/" y by LATTICE3:17 ;

assume A24: x "\/" (y "/\" z) = y ; :: thesis: contradiction

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: verum

end;.= x "\/" y by LATTICE3:17 ;

assume A24: x "\/" (y "/\" z) = y ; :: thesis: contradiction

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: verum

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

now :: thesis: not x "\/" y = x "\/" (y "/\" z)

hence
x "\/" (y "/\" z) <> x "\/" y
; :: thesis: ( not y = (x "\/" y) "/\" z & not y = x "\/" y & not (x "\/" y) "/\" z = x "\/" y & (y "/\" z) "/\" (x "\/" (y "/\" z)) = y "/\" z & (y "/\" z) "/\" y = y "/\" z & y "/\" (x "\/" y) = y & ((x "\/" y) "/\" z) "/\" (x "\/" y) = (x "\/" y) "/\" z & (x "\/" (y "/\" z)) "/\" y = y "/\" z & (x "\/" (y "/\" z)) "/\" ((x "\/" y) "/\" z) = x "\/" (y "/\" z) & y "/\" ((x "\/" y) "/\" z) = y "/\" z & (x "\/" (y "/\" z)) "\/" y = x "\/" y & y "\/" ((x "\/" y) "/\" z) = x "\/" y )assume
x "\/" y = x "\/" (y "/\" z)
; :: thesis: contradiction

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: verum

end;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: verum

now :: thesis: not y = (x "\/" y) "/\" z

hence
y <> (x "\/" y) "/\" z
; :: thesis: ( not y = x "\/" y & not (x "\/" y) "/\" z = x "\/" y & (y "/\" z) "/\" (x "\/" (y "/\" z)) = y "/\" z & (y "/\" z) "/\" y = y "/\" z & y "/\" (x "\/" y) = y & ((x "\/" y) "/\" z) "/\" (x "\/" y) = (x "\/" y) "/\" z & (x "\/" (y "/\" z)) "/\" y = y "/\" z & (x "\/" (y "/\" z)) "/\" ((x "\/" y) "/\" z) = x "\/" (y "/\" z) & y "/\" ((x "\/" y) "/\" z) = y "/\" z & (x "\/" (y "/\" z)) "\/" y = x "\/" y & y "\/" ((x "\/" y) "/\" z) = x "\/" y )A27: y "/\" ((x "\/" y) "/\" z) =
((x "\/" y) "/\" y) "/\" z
by LATTICE3:16

.= y "/\" z by LATTICE3:18 ;

assume A28: y = (x "\/" y) "/\" z ; :: thesis: contradiction

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: verum

end;.= y "/\" z by LATTICE3:18 ;

assume A28: y = (x "\/" y) "/\" z ; :: thesis: contradiction

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: verum

now :: thesis: not y = x "\/" y

hence
y <> x "\/" y
; :: thesis: ( not (x "\/" y) "/\" z = x "\/" y & (y "/\" z) "/\" (x "\/" (y "/\" z)) = y "/\" z & (y "/\" z) "/\" y = y "/\" z & y "/\" (x "\/" y) = y & ((x "\/" y) "/\" z) "/\" (x "\/" y) = (x "\/" y) "/\" z & (x "\/" (y "/\" z)) "/\" y = y "/\" z & (x "\/" (y "/\" z)) "/\" ((x "\/" y) "/\" z) = x "\/" (y "/\" z) & y "/\" ((x "\/" y) "/\" z) = y "/\" z & (x "\/" (y "/\" z)) "\/" y = x "\/" y & y "\/" ((x "\/" y) "/\" z) = x "\/" y )assume A30:
y = x "\/" y
; :: thesis: contradiction

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: verum

end;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: verum

now :: thesis: not (x "\/" y) "/\" z = x "\/" y

hence
(x "\/" y) "/\" z <> x "\/" y
; :: thesis: ( (y "/\" z) "/\" (x "\/" (y "/\" z)) = y "/\" z & (y "/\" z) "/\" y = y "/\" z & y "/\" (x "\/" y) = y & ((x "\/" y) "/\" z) "/\" (x "\/" y) = (x "\/" y) "/\" z & (x "\/" (y "/\" z)) "/\" y = y "/\" z & (x "\/" (y "/\" z)) "/\" ((x "\/" y) "/\" z) = x "\/" (y "/\" z) & y "/\" ((x "\/" y) "/\" z) = y "/\" z & (x "\/" (y "/\" z)) "\/" y = x "\/" y & y "\/" ((x "\/" y) "/\" z) = x "\/" y )A31:
y <= x "\/" y
by YELLOW_0:22;

assume A32: (x "\/" y) "/\" z = x "\/" y ; :: thesis: contradiction

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: verum

end;assume A32: (x "\/" y) "/\" z = x "\/" y ; :: thesis: contradiction

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: verum

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 = y "/\" z & y "/\" (x "\/" y) = y & ((x "\/" y) "/\" z) "/\" (x "\/" y) = (x "\/" y) "/\" z & (x "\/" (y "/\" z)) "/\" y = y "/\" z & (x "\/" (y "/\" z)) "/\" ((x "\/" y) "/\" z) = x "\/" (y "/\" z) & y "/\" ((x "\/" y) "/\" z) = y "/\" z & (x "\/" (y "/\" z)) "\/" y = x "\/" y & y "\/" ((x "\/" y) "/\" z) = x "\/" y )

y "/\" z <= y by YELLOW_0:23;

hence (y "/\" z) "/\" y = y "/\" z by YELLOW_5:10; :: thesis: ( y "/\" (x "\/" y) = y & ((x "\/" y) "/\" z) "/\" (x "\/" y) = (x "\/" y) "/\" z & (x "\/" (y "/\" z)) "/\" y = y "/\" z & (x "\/" (y "/\" z)) "/\" ((x "\/" y) "/\" z) = x "\/" (y "/\" z) & y "/\" ((x "\/" y) "/\" z) = y "/\" z & (x "\/" (y "/\" z)) "\/" y = x "\/" y & y "\/" ((x "\/" y) "/\" z) = x "\/" y )

y <= x "\/" y by YELLOW_0:22;

hence y "/\" (x "\/" y) = y by YELLOW_5:10; :: thesis: ( ((x "\/" y) "/\" z) "/\" (x "\/" y) = (x "\/" y) "/\" z & (x "\/" (y "/\" z)) "/\" y = y "/\" z & (x "\/" (y "/\" z)) "/\" ((x "\/" y) "/\" z) = x "\/" (y "/\" z) & y "/\" ((x "\/" y) "/\" z) = y "/\" z & (x "\/" (y "/\" z)) "\/" y = x "\/" y & y "\/" ((x "\/" y) "/\" z) = x "\/" y )

(x "\/" y) "/\" z <= x "\/" y by YELLOW_0:23;

hence ((x "\/" y) "/\" z) "/\" (x "\/" y) = (x "\/" y) "/\" z by YELLOW_5:10; :: thesis: ( (x "\/" (y "/\" z)) "/\" y = y "/\" z & (x "\/" (y "/\" z)) "/\" ((x "\/" y) "/\" z) = x "\/" (y "/\" z) & y "/\" ((x "\/" y) "/\" z) = y "/\" z & (x "\/" (y "/\" z)) "\/" y = x "\/" y & y "\/" ((x "\/" y) "/\" z) = x "\/" y )

thus (x "\/" (y "/\" z)) "/\" y = y "/\" z by A16, A13, YELLOW_0:def 3; :: thesis: ( (x "\/" (y "/\" z)) "/\" ((x "\/" y) "/\" z) = x "\/" (y "/\" z) & y "/\" ((x "\/" y) "/\" z) = y "/\" z & (x "\/" (y "/\" z)) "\/" y = x "\/" y & y "\/" ((x "\/" y) "/\" z) = x "\/" y )

thus (x "\/" (y "/\" z)) "/\" ((x "\/" y) "/\" z) = x "\/" (y "/\" z) by A8, Th8, YELLOW_5:10; :: thesis: ( y "/\" ((x "\/" y) "/\" z) = y "/\" z & (x "\/" (y "/\" z)) "\/" y = x "\/" y & y "\/" ((x "\/" y) "/\" z) = x "\/" y )

thus y "/\" ((x "\/" y) "/\" z) = (y "/\" (x "\/" y)) "/\" z by LATTICE3:16

.= y "/\" z by LATTICE3:18 ; :: thesis: ( (x "\/" (y "/\" z)) "\/" y = x "\/" y & y "\/" ((x "\/" y) "/\" z) = x "\/" y )

thus (x "\/" (y "/\" z)) "\/" y = x "\/" ((y "/\" z) "\/" y) by LATTICE3:14

.= x "\/" y by LATTICE3:17 ; :: thesis: y "\/" ((x "\/" y) "/\" z) = x "\/" 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 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: verum

( 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: verum