let L be LATTICE; :: thesis: ( L is modular implies ( L is distributive iff 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 a "/\" d = a or not b "/\" e = b or not c "/\" e = c or not d "/\" e = d or not b "/\" c = a or not b "/\" d = a or not c "/\" d = a or not b "\/" c = e or not b "\/" d = e or not c "\/" d = e ) ) )
assume A1: L is modular ; :: thesis: ( L is distributive iff 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 a "/\" d = a or not b "/\" e = b or not c "/\" e = c or not d "/\" e = d or not b "/\" c = a or not b "/\" d = a or not c "/\" d = a or not b "\/" c = e or not b "\/" d = e or not c "\/" d = e ) )
now
given a, b, c, d, e being Element of L such that a <> b and
a <> c and
A2: a <> d and
a <> e and
b <> c and
b <> d and
b <> e and
c <> d and
c <> e and
d <> e and
a "/\" b = a and
a "/\" c = a and
a "/\" d = a and
b "/\" e = b and
c "/\" e = c and
A3: d "/\" e = d and
A4: b "/\" c = a and
A5: b "/\" d = a and
A6: c "/\" d = a and
A7: b "\/" c = e and
b "\/" d = e and
c "\/" d = e ; :: thesis: not L is distributive
(b "/\" c) "\/" (b "/\" d) = a by A4, A5, YELLOW_5:1;
hence not L is distributive by A2, A3, A4, A6, A7, WAYBEL_1:def 3; :: thesis: verum
end;
hence ( L is distributive 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 a "/\" d = a or not b "/\" e = b or not c "/\" e = c or not d "/\" e = d or not b "/\" c = a or not b "/\" d = a or not c "/\" d = a or not b "\/" c = e or not b "\/" d = e or not c "\/" d = e ) ) ; :: thesis: ( ( 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 a "/\" d = a or not b "/\" e = b or not c "/\" e = c or not d "/\" e = d or not b "/\" c = a or not b "/\" d = a or not c "/\" d = a or not b "\/" c = e or not b "\/" d = e or not c "\/" d = e ) ) implies L is distributive )
now
assume not L is distributive ; :: thesis: 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 & a "/\" d = a & b "/\" e = b & c "/\" e = c & d "/\" e = d & b "/\" c = a & b "/\" d = a & c "/\" d = a & b "\/" c = e & b "\/" d = e & c "\/" d = e )
then consider x, y, z being Element of L such that
A8: x "/\" (y "\/" z) <> (x "/\" y) "\/" (x "/\" z) by WAYBEL_1:def 3;
set t = ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x);
set b = ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x);
A9: x "/\" y <= x by YELLOW_0:23;
A10: x "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) = (x "/\" ((x "\/" y) "/\" (y "\/" z))) "/\" (z "\/" x) by LATTICE3:16
.= ((x "/\" (x "\/" y)) "/\" (y "\/" z)) "/\" (z "\/" x) by LATTICE3:16
.= (x "/\" (y "\/" z)) "/\" (z "\/" x) by LATTICE3:18
.= (x "/\" (z "\/" x)) "/\" (y "\/" z) by LATTICE3:16
.= x "/\" (y "\/" z) by LATTICE3:18 ;
A11: x <= x ;
y "/\" z <= z by YELLOW_0:23;
then A12: ((y "/\" z) "/\" x) "\/" (z "/\" x) = z "/\" x by A11, YELLOW_3:2, YELLOW_5:8;
A13: z "/\" x <= x by YELLOW_0:23;
A14: now
assume ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) = ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) ; :: thesis: contradiction
then x "/\" (y "\/" z) = ((x "/\" y) "\/" ((y "/\" z) "\/" (z "/\" x))) "/\" x by A10, LATTICE3:14
.= (x "/\" y) "\/" (((y "/\" z) "\/" (z "/\" x)) "/\" x) by A1, A9, Def3
.= (x "/\" y) "\/" (z "/\" x) by A1, A13, A12, Def3 ;
hence contradiction by A8; :: thesis: verum
end;
set y1 = (y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x));
A15: y "/\" z <= y "\/" z by YELLOW_5:5;
y "/\" z <= x "\/" y by YELLOW_5:5;
then (y "/\" z) "/\" (y "/\" z) <= (x "\/" y) "/\" (y "\/" z) by A15, YELLOW_3:2;
then A16: y "/\" z <= (x "\/" y) "/\" (y "\/" z) by YELLOW_5:2;
y "/\" z <= z "\/" x by YELLOW_5:5;
then (y "/\" z) "/\" (y "/\" z) <= ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) by A16, YELLOW_3:2;
then A17: y "/\" z <= ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) by YELLOW_5:2;
A18: x "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) = (x "/\" ((x "\/" y) "/\" (y "\/" z))) "/\" (z "\/" x) by LATTICE3:16
.= ((x "/\" (x "\/" y)) "/\" (y "\/" z)) "/\" (z "\/" x) by LATTICE3:16
.= (x "/\" (y "\/" z)) "/\" (z "\/" x) by LATTICE3:18
.= ((z "\/" x) "/\" x) "/\" (y "\/" z) by LATTICE3:16
.= x "/\" (y "\/" z) by LATTICE3:18 ;
set z1 = (z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x));
A19: z "/\" x <= y "\/" z by YELLOW_5:5;
z "/\" x <= x "\/" y by YELLOW_5:5;
then (z "/\" x) "/\" (z "/\" x) <= (x "\/" y) "/\" (y "\/" z) by A19, YELLOW_3:2;
then A20: z "/\" x <= (x "\/" y) "/\" (y "\/" z) by YELLOW_5:2;
z "/\" x <= z "\/" x by YELLOW_5:5;
then (z "/\" x) "/\" (z "/\" x) <= ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) by A20, YELLOW_3:2;
then A21: z "/\" x <= ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) by YELLOW_5:2;
A22: y "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) = (y "/\" ((x "\/" y) "/\" (y "\/" z))) "/\" (z "\/" x) by LATTICE3:16
.= ((y "/\" (x "\/" y)) "/\" (y "\/" z)) "/\" (z "\/" x) by LATTICE3:16
.= (y "/\" (y "\/" z)) "/\" (z "\/" x) by LATTICE3:18
.= y "/\" (x "\/" z) by LATTICE3:18 ;
A23: x <= x "\/" (y "/\" z) by YELLOW_0:22;
x "/\" z <= x by YELLOW_0:23;
then A24: x "/\" z <= x "\/" (y "/\" z) by A23, YELLOW_0:def 2;
A25: y <= y "\/" z by YELLOW_0:22;
A26: z "\/" (x "/\" y) <= (z "\/" x) "/\" (z "\/" y) by Th7;
A27: y "\/" (x "/\" z) <= (y "\/" x) "/\" (y "\/" z) by Th7;
A28: x <= x "\/" y by YELLOW_0:22;
x "/\" (z "\/" y) <= x by YELLOW_0:23;
then A29: x "/\" (z "\/" y) <= x "\/" y by A28, YELLOW_0:def 2;
A30: y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)) = (y "\/" ((x "/\" y) "\/" (y "/\" z))) "\/" (z "/\" x) by LATTICE3:14
.= ((y "\/" (x "/\" y)) "\/" (y "/\" z)) "\/" (z "/\" x) by LATTICE3:14
.= (y "\/" (y "/\" z)) "\/" (z "/\" x) by LATTICE3:17
.= y "\/" (x "/\" z) by LATTICE3:17 ;
A31: x <= x "\/" (z "/\" y) by YELLOW_0:22;
x "/\" y <= x by YELLOW_0:23;
then A32: x "/\" y <= x "\/" (z "/\" y) by A31, YELLOW_0:def 2;
A33: z <= z "\/" y by YELLOW_0:22;
A34: y "\/" (z "/\" x) <= (y "\/" z) "/\" (y "\/" x) by Th7;
A35: (x "/\" y) "\/" (y "/\" z) <= y "/\" (x "\/" z) by Th6;
A36: y "/\" z <= y by YELLOW_0:23;
A37: z <= z "\/" x by YELLOW_0:22;
z "/\" (y "\/" x) <= z by YELLOW_0:23;
then A38: z "/\" (y "\/" x) <= z "\/" x by A37, YELLOW_0:def 2;
A39: z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)) = (z "\/" (z "/\" x)) "\/" ((x "/\" y) "\/" (y "/\" z)) by LATTICE3:14
.= z "\/" ((y "/\" z) "\/" (x "/\" y)) by LATTICE3:17
.= (z "\/" (y "/\" z)) "\/" (x "/\" y) by LATTICE3:14
.= z "\/" (x "/\" y) by LATTICE3:17 ;
(x "/\" y) "\/" (x "/\" z) <= x "/\" (y "\/" z) by Th6;
then ((x "/\" y) "\/" (x "/\" z)) "\/" ((x "/\" y) "\/" (y "/\" z)) <= (x "/\" (y "\/" z)) "\/" (y "/\" (x "\/" z)) by A35, YELLOW_3:3;
then (x "/\" z) "\/" ((x "/\" y) "\/" ((x "/\" y) "\/" (y "/\" z))) <= (x "/\" (y "\/" z)) "\/" (y "/\" (x "\/" z)) by LATTICE3:14;
then (x "/\" z) "\/" (((x "/\" y) "\/" (x "/\" y)) "\/" (y "/\" z)) <= (x "/\" (y "\/" z)) "\/" (y "/\" (x "\/" z)) by LATTICE3:14;
then (((x "/\" y) "\/" (x "/\" y)) "\/" (x "/\" z)) "\/" (y "/\" z) <= (x "/\" (y "\/" z)) "\/" (y "/\" (x "\/" z)) by LATTICE3:14;
then ((x "/\" y) "\/" (x "/\" z)) "\/" (y "/\" z) <= (x "/\" (y "\/" z)) "\/" (y "/\" (x "\/" z)) by YELLOW_5:1;
then A40: ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) <= (x "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" (y "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) by A18, A22, LATTICE3:14;
(z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) <= ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) by YELLOW_0:23;
then A41: (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) "/\" ((z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) = (z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) by YELLOW_5:10;
A42: z <= z "\/" (y "/\" x) by YELLOW_0:22;
z "/\" x <= z by YELLOW_0:23;
then A43: z "/\" x <= z "\/" (y "/\" x) by A42, YELLOW_0:def 2;
A44: y <= y "\/" x by YELLOW_0:22;
A45: x <= x "\/" z by YELLOW_0:22;
x "/\" (y "\/" z) <= x by YELLOW_0:23;
then A46: x "/\" (y "\/" z) <= x "\/" z by A45, YELLOW_0:def 2;
A47: x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)) = (x "\/" ((x "/\" y) "\/" (y "/\" z))) "\/" (z "/\" x) by LATTICE3:14
.= ((x "\/" (x "/\" y)) "\/" (y "/\" z)) "\/" (z "/\" x) by LATTICE3:14
.= (x "\/" (y "/\" z)) "\/" (z "/\" x) by LATTICE3:17
.= ((z "/\" x) "\/" x) "\/" (y "/\" z) by LATTICE3:14
.= x "\/" (y "/\" z) by LATTICE3:17 ;
z "\/" (y "/\" x) <= (z "\/" y) "/\" (z "\/" x) by Th7;
then (z "\/" (y "/\" x)) "/\" (y "\/" (z "/\" x)) <= ((z "\/" y) "/\" (z "\/" x)) "/\" ((y "\/" z) "/\" (y "\/" x)) by A34, YELLOW_3:2;
then (z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) <= (((z "\/" x) "/\" (z "\/" y)) "/\" (z "\/" y)) "/\" (y "\/" x) by A30, A39, LATTICE3:16;
then (z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) <= ((z "\/" x) "/\" ((z "\/" y) "/\" (z "\/" y))) "/\" (y "\/" x) by LATTICE3:16;
then (z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) <= ((z "\/" x) "/\" (z "\/" y)) "/\" (y "\/" x) by YELLOW_5:2;
then A48: (z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) <= ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) by LATTICE3:16;
(y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) <= ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) by YELLOW_0:23;
then A49: (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) "/\" ((y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) = (y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) by YELLOW_5:10;
set x1 = (x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x));
A50: x "/\" y <= y "\/" z by YELLOW_5:5;
x "/\" y <= x "\/" y by YELLOW_5:5;
then (x "/\" y) "/\" (x "/\" y) <= (x "\/" y) "/\" (y "\/" z) by A50, YELLOW_3:2;
then A51: x "/\" y <= (x "\/" y) "/\" (y "\/" z) by YELLOW_5:2;
A52: z "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) = (z "/\" (z "\/" x)) "/\" ((x "\/" y) "/\" (y "\/" z)) by LATTICE3:16
.= z "/\" ((y "\/" z) "/\" (x "\/" y)) by LATTICE3:18
.= (z "/\" (y "\/" z)) "/\" (x "\/" y) by LATTICE3:16
.= z "/\" (x "\/" y) by LATTICE3:18 ;
x "\/" (y "/\" z) <= (x "\/" y) "/\" (x "\/" z) by Th7;
then (x "\/" (y "/\" z)) "/\" (y "\/" (x "/\" z)) <= ((x "\/" y) "/\" (x "\/" z)) "/\" ((y "\/" x) "/\" (y "\/" z)) by A27, YELLOW_3:2;
then (x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) <= (((x "\/" z) "/\" (x "\/" y)) "/\" (x "\/" y)) "/\" (y "\/" z) by A47, A30, LATTICE3:16;
then (x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) <= ((x "\/" z) "/\" ((x "\/" y) "/\" (x "\/" y))) "/\" (y "\/" z) by LATTICE3:16;
then (x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) <= ((x "\/" z) "/\" (x "\/" y)) "/\" (y "\/" z) by YELLOW_5:2;
then A53: (x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) <= ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) by LATTICE3:16;
A54: (z "/\" y) "\/" (y "/\" x) <= y "/\" (z "\/" x) by Th6;
A55: y "/\" x <= y by YELLOW_0:23;
A56: ((x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "/\" ((y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) = (x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" ((((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) "/\" ((y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)))) by LATTICE3:16
.= (x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "/\" (y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)))) by LATTICE3:16
.= (x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" ((y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) by YELLOW_5:2
.= ((x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) by LATTICE3:16
.= (x "\/" (y "/\" z)) "/\" (y "\/" (x "/\" z)) by A47, A30, A53, YELLOW_5:10
.= (y "/\" (x "\/" (y "/\" z))) "\/" (x "/\" z) by A1, A24, Def3
.= ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) by A1, A36, Def3 ;
then ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) <= (y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) by YELLOW_0:23;
then A57: (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)) "\/" ((y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) = (y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) by YELLOW_5:8;
x "\/" (z "/\" y) <= (x "\/" z) "/\" (x "\/" y) by Th7;
then (x "\/" (z "/\" y)) "/\" (z "\/" (x "/\" y)) <= ((x "\/" z) "/\" (x "\/" y)) "/\" ((z "\/" x) "/\" (z "\/" y)) by A26, YELLOW_3:2;
then (x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) <= (((x "\/" y) "/\" (x "\/" z)) "/\" (x "\/" z)) "/\" (z "\/" y) by A47, A39, LATTICE3:16;
then (x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) <= ((x "\/" y) "/\" ((x "\/" z) "/\" (x "\/" z))) "/\" (z "\/" y) by LATTICE3:16;
then (x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) <= ((x "\/" y) "/\" (x "\/" z)) "/\" (z "\/" y) by YELLOW_5:2;
then A58: (x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) <= ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) by LATTICE3:16;
(x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) <= ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) by YELLOW_0:23;
then A59: (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) "/\" ((x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) = (x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) by YELLOW_5:10;
A60: ((z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "/\" ((y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) = (z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" ((((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) "/\" ((y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)))) by LATTICE3:16
.= (z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "/\" (y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)))) by LATTICE3:16
.= (z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" ((y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) by YELLOW_5:2
.= ((z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) by LATTICE3:16
.= (z "\/" (y "/\" x)) "/\" (y "\/" (z "/\" x)) by A30, A39, A48, YELLOW_5:10
.= (y "/\" (z "\/" (y "/\" x))) "\/" (z "/\" x) by A1, A43, Def3
.= ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) by A1, A55, Def3 ;
(z "/\" y) "\/" (z "/\" x) <= z "/\" (y "\/" x) by Th6;
then ((z "/\" y) "\/" (z "/\" x)) "\/" ((z "/\" y) "\/" (y "/\" x)) <= (z "/\" (y "\/" x)) "\/" (y "/\" (z "\/" x)) by A54, YELLOW_3:3;
then (z "/\" x) "\/" ((z "/\" y) "\/" ((z "/\" y) "\/" (y "/\" x))) <= (z "/\" (y "\/" x)) "\/" (y "/\" (z "\/" x)) by LATTICE3:14;
then (z "/\" x) "\/" (((z "/\" y) "\/" (z "/\" y)) "\/" (y "/\" x)) <= (z "/\" (y "\/" x)) "\/" (y "/\" (z "\/" x)) by LATTICE3:14;
then (((z "/\" y) "\/" (z "/\" y)) "\/" (z "/\" x)) "\/" (y "/\" x) <= (z "/\" (y "\/" x)) "\/" (y "/\" (z "\/" x)) by LATTICE3:14;
then ((z "/\" y) "\/" (z "/\" x)) "\/" (y "/\" x) <= (z "/\" (y "\/" x)) "\/" (y "/\" (z "\/" x)) by YELLOW_5:1;
then A61: ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) <= (z "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" (y "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) by A22, A52, LATTICE3:14;
A62: (x "/\" z) "\/" (z "/\" y) <= z "/\" (x "\/" y) by Th6;
A63: z "/\" y <= z by YELLOW_0:23;
(x "/\" z) "\/" (x "/\" y) <= x "/\" (z "\/" y) by Th6;
then ((x "/\" z) "\/" (x "/\" y)) "\/" ((x "/\" z) "\/" (z "/\" y)) <= (x "/\" (z "\/" y)) "\/" (z "/\" (x "\/" y)) by A62, YELLOW_3:3;
then (x "/\" y) "\/" ((x "/\" z) "\/" ((x "/\" z) "\/" (z "/\" y))) <= (x "/\" (z "\/" y)) "\/" (z "/\" (x "\/" y)) by LATTICE3:14;
then (x "/\" y) "\/" (((x "/\" z) "\/" (x "/\" z)) "\/" (z "/\" y)) <= (x "/\" (z "\/" y)) "\/" (z "/\" (x "\/" y)) by LATTICE3:14;
then (((x "/\" z) "\/" (x "/\" z)) "\/" (x "/\" y)) "\/" (z "/\" y) <= (x "/\" (z "\/" y)) "\/" (z "/\" (x "\/" y)) by LATTICE3:14;
then ((x "/\" z) "\/" (x "/\" y)) "\/" (z "/\" y) <= (x "/\" (z "\/" y)) "\/" (z "/\" (x "\/" y)) by YELLOW_5:1;
then A64: ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) <= (x "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" (z "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) by A18, A52, LATTICE3:14;
x "/\" y <= z "\/" x by YELLOW_5:5;
then (x "/\" y) "/\" (x "/\" y) <= ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) by A51, YELLOW_3:2;
then x "/\" y <= ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) by YELLOW_5:2;
then (x "/\" y) "\/" (y "/\" z) <= (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) "\/" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) by A17, YELLOW_3:3;
then (x "/\" y) "\/" (y "/\" z) <= ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) by YELLOW_5:1;
then ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) <= (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) "\/" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) by A21, YELLOW_3:3;
then A65: ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) <= ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) by YELLOW_5:1;
then (z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) = (z "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)) by A1, Def3;
then A66: ((x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" ((z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) = ((x "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "\/" ((z "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) by A1, A65, Def3
.= (x "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" ((((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)) "\/" ((z "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)))) by LATTICE3:14
.= (x "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" (((((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)) "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "\/" (z "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)))) by LATTICE3:14
.= (x "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" ((z "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) by YELLOW_5:1
.= ((x "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" (z "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)))) "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)) by LATTICE3:14
.= (x "/\" (z "\/" y)) "\/" (z "/\" (x "\/" y)) by A18, A52, A64, YELLOW_5:8
.= (z "\/" (x "/\" (z "\/" y))) "/\" (x "\/" y) by A1, A29, Def3
.= ((z "\/" x) "/\" (z "\/" y)) "/\" (x "\/" y) by A1, A33, Def3
.= ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) by LATTICE3:16 ;
A67: (y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) = (y "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)) by A1, A65, Def3;
then A68: ((x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" ((y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) = ((x "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "\/" ((y "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) by A1, A65, Def3
.= (x "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" ((((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)) "\/" ((y "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)))) by LATTICE3:14
.= (x "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" (((((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)) "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "\/" (y "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)))) by LATTICE3:14
.= (x "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" ((y "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) by YELLOW_5:1
.= ((x "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" (y "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)))) "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)) by LATTICE3:14
.= (x "/\" (y "\/" z)) "\/" (y "/\" (x "\/" z)) by A18, A22, A40, YELLOW_5:8
.= (y "\/" (x "/\" (y "\/" z))) "/\" (x "\/" z) by A1, A46, Def3
.= ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) by A1, A25, Def3 ;
A69: ((z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" ((y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) = ((z "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "\/" ((y "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) by A1, A65, A67, Def3
.= (z "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" ((((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)) "\/" ((y "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)))) by LATTICE3:14
.= (z "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" (((((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)) "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "\/" (y "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)))) by LATTICE3:14
.= (z "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" ((y "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) by YELLOW_5:1
.= ((z "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" (y "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)))) "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)) by LATTICE3:14
.= (z "/\" (y "\/" x)) "\/" (y "/\" (z "\/" x)) by A22, A52, A61, YELLOW_5:8
.= (y "\/" (z "/\" (y "\/" x))) "/\" (z "\/" x) by A1, A38, Def3
.= ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) by A1, A44, Def3 ;
A70: ((x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "/\" ((z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) = (x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" ((((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) "/\" ((z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)))) by LATTICE3:16
.= (x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "/\" (z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)))) by LATTICE3:16
.= (x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" ((z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) by YELLOW_5:2
.= ((x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) by LATTICE3:16
.= (x "\/" (z "/\" y)) "/\" (z "\/" (x "/\" y)) by A47, A39, A58, YELLOW_5:10
.= (z "/\" (x "\/" (z "/\" y))) "\/" (x "/\" y) by A1, A32, Def3
.= ((z "/\" x) "\/" (z "/\" y)) "\/" (x "/\" y) by A1, A63, Def3
.= ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) by LATTICE3:14 ;
then ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) <= (z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) by YELLOW_0:23;
then A71: (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)) "\/" ((z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) = (z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) by YELLOW_5:8;
((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) <= (x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) by A56, YELLOW_0:23;
then A72: (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)) "\/" ((x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) = (x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) by YELLOW_5:8;
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 & a "/\" d = a & b "/\" e = b & c "/\" e = c & d "/\" e = d & b "/\" c = a & b "/\" d = a & c "/\" d = a & b "\/" c = e & b "\/" d = e & c "\/" d = e ) :: thesis: verum
proof
reconsider b = ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x), x1 = (x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)), y1 = (y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)), z1 = (z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)), t = ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) as Element of L ;
take b ; :: thesis: ex b, c, d, e being Element of L st
( b <> b & b <> c & b <> d & b <> e & b <> c & b <> d & b <> e & c <> d & c <> e & d <> e & b "/\" b = b & b "/\" c = b & b "/\" d = b & b "/\" e = b & c "/\" e = c & d "/\" e = d & b "/\" c = b & b "/\" d = b & c "/\" d = b & b "\/" c = e & b "\/" d = e & c "\/" d = e )
take x1 ; :: thesis: ex c, d, e being Element of L st
( b <> x1 & b <> c & b <> d & b <> e & x1 <> c & x1 <> d & x1 <> e & c <> d & c <> e & d <> e & b "/\" x1 = b & b "/\" c = b & b "/\" d = b & x1 "/\" e = x1 & c "/\" e = c & d "/\" e = d & x1 "/\" c = b & x1 "/\" d = b & c "/\" d = b & x1 "\/" c = e & x1 "\/" d = e & c "\/" d = e )
take y1 ; :: thesis: ex d, e being Element of L st
( b <> x1 & b <> y1 & b <> d & b <> e & x1 <> y1 & x1 <> d & x1 <> e & y1 <> d & y1 <> e & d <> e & b "/\" x1 = b & b "/\" y1 = b & b "/\" d = b & x1 "/\" e = x1 & y1 "/\" e = y1 & d "/\" e = d & x1 "/\" y1 = b & x1 "/\" d = b & y1 "/\" d = b & x1 "\/" y1 = e & x1 "\/" d = e & y1 "\/" d = e )
take z1 ; :: thesis: ex e being Element of L st
( b <> x1 & b <> y1 & b <> z1 & b <> e & x1 <> y1 & x1 <> z1 & x1 <> e & y1 <> z1 & y1 <> e & z1 <> e & b "/\" x1 = b & b "/\" y1 = b & b "/\" z1 = b & x1 "/\" e = x1 & y1 "/\" e = y1 & z1 "/\" e = z1 & x1 "/\" y1 = b & x1 "/\" z1 = b & y1 "/\" z1 = b & x1 "\/" y1 = e & x1 "\/" z1 = e & y1 "\/" z1 = e )
take t ; :: thesis: ( b <> x1 & b <> y1 & b <> z1 & b <> t & x1 <> y1 & x1 <> z1 & x1 <> t & y1 <> z1 & y1 <> t & z1 <> t & b "/\" x1 = b & b "/\" y1 = b & b "/\" z1 = b & x1 "/\" t = x1 & y1 "/\" t = y1 & z1 "/\" t = z1 & x1 "/\" y1 = b & x1 "/\" z1 = b & y1 "/\" z1 = b & x1 "\/" y1 = t & x1 "\/" z1 = t & y1 "\/" z1 = t )
thus b <> x1 by A14, A68, A66, A60, A57, A71, YELLOW_5:2; :: thesis: ( b <> y1 & b <> z1 & b <> t & x1 <> y1 & x1 <> z1 & x1 <> t & y1 <> z1 & y1 <> t & z1 <> t & b "/\" x1 = b & b "/\" y1 = b & b "/\" z1 = b & x1 "/\" t = x1 & y1 "/\" t = y1 & z1 "/\" t = z1 & x1 "/\" y1 = b & x1 "/\" z1 = b & y1 "/\" z1 = b & x1 "\/" y1 = t & x1 "\/" z1 = t & y1 "\/" z1 = t )
thus b <> y1 by A14, A68, A70, A69, A72, A71, YELLOW_5:2; :: thesis: ( b <> z1 & b <> t & x1 <> y1 & x1 <> z1 & x1 <> t & y1 <> z1 & y1 <> t & z1 <> t & b "/\" x1 = b & b "/\" y1 = b & b "/\" z1 = b & x1 "/\" t = x1 & y1 "/\" t = y1 & z1 "/\" t = z1 & x1 "/\" y1 = b & x1 "/\" z1 = b & y1 "/\" z1 = b & x1 "\/" y1 = t & x1 "\/" z1 = t & y1 "\/" z1 = t )
thus b <> z1 by A14, A56, A66, A69, A72, A57, YELLOW_5:2; :: thesis: ( b <> t & x1 <> y1 & x1 <> z1 & x1 <> t & y1 <> z1 & y1 <> t & z1 <> t & b "/\" x1 = b & b "/\" y1 = b & b "/\" z1 = b & x1 "/\" t = x1 & y1 "/\" t = y1 & z1 "/\" t = z1 & x1 "/\" y1 = b & x1 "/\" z1 = b & y1 "/\" z1 = b & x1 "\/" y1 = t & x1 "\/" z1 = t & y1 "\/" z1 = t )
thus b <> t by A14; :: thesis: ( x1 <> y1 & x1 <> z1 & x1 <> t & y1 <> z1 & y1 <> t & z1 <> t & b "/\" x1 = b & b "/\" y1 = b & b "/\" z1 = b & x1 "/\" t = x1 & y1 "/\" t = y1 & z1 "/\" t = z1 & x1 "/\" y1 = b & x1 "/\" z1 = b & y1 "/\" z1 = b & x1 "\/" y1 = t & x1 "\/" z1 = t & y1 "\/" z1 = t )
hence x1 <> y1 ; :: thesis: ( x1 <> z1 & x1 <> t & y1 <> z1 & y1 <> t & z1 <> t & b "/\" x1 = b & b "/\" y1 = b & b "/\" z1 = b & x1 "/\" t = x1 & y1 "/\" t = y1 & z1 "/\" t = z1 & x1 "/\" y1 = b & x1 "/\" z1 = b & y1 "/\" z1 = b & x1 "\/" y1 = t & x1 "\/" z1 = t & y1 "\/" z1 = t )
hence x1 <> z1 ; :: thesis: ( x1 <> t & y1 <> z1 & y1 <> t & z1 <> t & b "/\" x1 = b & b "/\" y1 = b & b "/\" z1 = b & x1 "/\" t = x1 & y1 "/\" t = y1 & z1 "/\" t = z1 & x1 "/\" y1 = b & x1 "/\" z1 = b & y1 "/\" z1 = b & x1 "\/" y1 = t & x1 "\/" z1 = t & y1 "\/" z1 = t )
thus x1 <> t by A14, A56, A70, A69, A49, A41, YELLOW_5:1; :: thesis: ( y1 <> z1 & y1 <> t & z1 <> t & b "/\" x1 = b & b "/\" y1 = b & b "/\" z1 = b & x1 "/\" t = x1 & y1 "/\" t = y1 & z1 "/\" t = z1 & x1 "/\" y1 = b & x1 "/\" z1 = b & y1 "/\" z1 = b & x1 "\/" y1 = t & x1 "\/" z1 = t & y1 "\/" z1 = t )
hence y1 <> z1 ; :: thesis: ( y1 <> t & z1 <> t & b "/\" x1 = b & b "/\" y1 = b & b "/\" z1 = b & x1 "/\" t = x1 & y1 "/\" t = y1 & z1 "/\" t = z1 & x1 "/\" y1 = b & x1 "/\" z1 = b & y1 "/\" z1 = b & x1 "\/" y1 = t & x1 "\/" z1 = t & y1 "\/" z1 = t )
thus y1 <> t by A14, A56, A66, A60, A59, A41, YELLOW_5:1; :: thesis: ( z1 <> t & b "/\" x1 = b & b "/\" y1 = b & b "/\" z1 = b & x1 "/\" t = x1 & y1 "/\" t = y1 & z1 "/\" t = z1 & x1 "/\" y1 = b & x1 "/\" z1 = b & y1 "/\" z1 = b & x1 "\/" y1 = t & x1 "\/" z1 = t & y1 "\/" z1 = t )
thus z1 <> t by A14, A68, A70, A60, A59, A49, YELLOW_5:1; :: thesis: ( b "/\" x1 = b & b "/\" y1 = b & b "/\" z1 = b & x1 "/\" t = x1 & y1 "/\" t = y1 & z1 "/\" t = z1 & x1 "/\" y1 = b & x1 "/\" z1 = b & y1 "/\" z1 = b & x1 "\/" y1 = t & x1 "\/" z1 = t & y1 "\/" z1 = t )
b <= x1 by A56, YELLOW_0:23;
hence b "/\" x1 = b by YELLOW_5:10; :: thesis: ( b "/\" y1 = b & b "/\" z1 = b & x1 "/\" t = x1 & y1 "/\" t = y1 & z1 "/\" t = z1 & x1 "/\" y1 = b & x1 "/\" z1 = b & y1 "/\" z1 = b & x1 "\/" y1 = t & x1 "\/" z1 = t & y1 "\/" z1 = t )
b <= y1 by A56, YELLOW_0:23;
hence b "/\" y1 = b by YELLOW_5:10; :: thesis: ( b "/\" z1 = b & x1 "/\" t = x1 & y1 "/\" t = y1 & z1 "/\" t = z1 & x1 "/\" y1 = b & x1 "/\" z1 = b & y1 "/\" z1 = b & x1 "\/" y1 = t & x1 "\/" z1 = t & y1 "\/" z1 = t )
b <= z1 by A70, YELLOW_0:23;
hence b "/\" z1 = b by YELLOW_5:10; :: thesis: ( x1 "/\" t = x1 & y1 "/\" t = y1 & z1 "/\" t = z1 & x1 "/\" y1 = b & x1 "/\" z1 = b & y1 "/\" z1 = b & x1 "\/" y1 = t & x1 "\/" z1 = t & y1 "\/" z1 = t )
x1 <= t by A68, YELLOW_0:22;
hence x1 "/\" t = x1 by YELLOW_5:10; :: thesis: ( y1 "/\" t = y1 & z1 "/\" t = z1 & x1 "/\" y1 = b & x1 "/\" z1 = b & y1 "/\" z1 = b & x1 "\/" y1 = t & x1 "\/" z1 = t & y1 "\/" z1 = t )
y1 <= t by A68, YELLOW_0:22;
hence y1 "/\" t = y1 by YELLOW_5:10; :: thesis: ( z1 "/\" t = z1 & x1 "/\" y1 = b & x1 "/\" z1 = b & y1 "/\" z1 = b & x1 "\/" y1 = t & x1 "\/" z1 = t & y1 "\/" z1 = t )
z1 <= t by A66, YELLOW_0:22;
hence z1 "/\" t = z1 by YELLOW_5:10; :: thesis: ( x1 "/\" y1 = b & x1 "/\" z1 = b & y1 "/\" z1 = b & x1 "\/" y1 = t & x1 "\/" z1 = t & y1 "\/" z1 = t )
thus x1 "/\" y1 = b by A56; :: thesis: ( x1 "/\" z1 = b & y1 "/\" z1 = b & x1 "\/" y1 = t & x1 "\/" z1 = t & y1 "\/" z1 = t )
thus x1 "/\" z1 = b by A70; :: thesis: ( y1 "/\" z1 = b & x1 "\/" y1 = t & x1 "\/" z1 = t & y1 "\/" z1 = t )
thus y1 "/\" z1 = b by A60; :: thesis: ( x1 "\/" y1 = t & x1 "\/" z1 = t & y1 "\/" z1 = t )
thus x1 "\/" y1 = t by A68; :: thesis: ( x1 "\/" z1 = t & y1 "\/" z1 = t )
thus x1 "\/" z1 = t by A66; :: thesis: y1 "\/" z1 = t
thus y1 "\/" z1 = t by A69; :: thesis: verum
end;
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 a "/\" d = a or not b "/\" e = b or not c "/\" e = c or not d "/\" e = d or not b "/\" c = a or not b "/\" d = a or not c "/\" d = a or not b "\/" c = e or not b "\/" d = e or not c "\/" d = e ) ) implies L is distributive ) ; :: thesis: verum