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

proof

now

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

end;

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
A4: x "/\" (y "\/" z) <> (x "/\" y) "\/" (x "/\" z) by WAYBEL_1:def 3;
set b = ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x);
set t = ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x);
A5: ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) <= ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)

proof

A6: ( x "/\" y <= x "\/" y & x "/\" y <= y "\/" z & x "/\" y <= z "\/" x ) by YELLOW_5:5;
A7: ( y "/\" z <= x "\/" y & y "/\" z <= y "\/" z & y "/\" z <= z "\/" x ) by YELLOW_5:5;
A8: ( z "/\" x <= x "\/" y & z "/\" x <= y "\/" z & z "/\" x <= z "\/" x ) by YELLOW_5:5;
(x "/\" y) "/\" (x "/\" y) <= (x "\/" y) "/\" (y "\/" z) by A6, YELLOW_3:2;
then x "/\" y <= (x "\/" y) "/\" (y "\/" z) by YELLOW_5:2;
then (x "/\" y) "/\" (x "/\" y) <= ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) by A6, YELLOW_3:2;
then A9: x "/\" y <= ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) by YELLOW_5:2;
(y "/\" z) "/\" (y "/\" z) <= (x "\/" y) "/\" (y "\/" z) by A7, YELLOW_3:2;
then y "/\" z <= (x "\/" y) "/\" (y "\/" z) by YELLOW_5:2;
then (y "/\" z) "/\" (y "/\" z) <= ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) by A7, YELLOW_3:2;
then A10: y "/\" z <= ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) by YELLOW_5:2;
(z "/\" x) "/\" (z "/\" x) <= (x "\/" y) "/\" (y "\/" z) by A8, YELLOW_3:2;
then z "/\" x <= (x "\/" y) "/\" (y "\/" z) by YELLOW_5:2;
then (z "/\" x) "/\" (z "/\" x) <= ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) by A8, YELLOW_3:2;
then A11: z "/\" x <= ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) by YELLOW_5:2;
(x "/\" y) "\/" (y "/\" z) <= (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) "\/" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) by A9, A10, 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 A11, YELLOW_3:3;
hence ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) <= ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) by YELLOW_5:1; :: thesis: verum

end;

A12: ( z "/\" x <= x & x "/\" y <= x ) by YELLOW_0:23;
( y "/\" z <= z & x <= x ) by YELLOW_0:23;
then A13: ((y "/\" z) "/\" x) "\/" (z "/\" x) = z "/\" x by YELLOW_3:2, YELLOW_5:8;
A14: 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 ;
A15: ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) <> ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)

proof

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 A14, LATTICE3:14
.= (x "/\" y) "\/" (((y "/\" z) "\/" (z "/\" x)) "/\" x) by A1, A12, Def3
.= (x "/\" y) "\/" (z "/\" x) by A1, A12, A13, Def3 ;
hence contradiction by A4; :: thesis: verum

end;

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

end;

set x1 = (x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x));
set y1 = (y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x));
set z1 = (z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x));
A16: 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 ;
A17: 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 ;
A18: 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 ;
A19: 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 ;
A20: 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 ;
A21: 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 ;
A22: ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) <= (x "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" (y "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)))

proof

( (x "/\" y) "\/" (x "/\" z) <= x "/\" (y "\/" z) & (x "/\" y) "\/" (y "/\" z) <= y "/\" (x "\/" z) ) by Th6;
then ((x "/\" y) "\/" (x "/\" z)) "\/" ((x "/\" y) "\/" (y "/\" z)) <= (x "/\" (y "\/" z)) "\/" (y "/\" (x "\/" z)) by 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;
hence ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) <= (x "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" (y "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) by A16, A17, LATTICE3:14; :: thesis: verum

end;

A23: ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) <= (x "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" (z "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)))

proof

( (x "/\" z) "\/" (x "/\" y) <= x "/\" (z "\/" y) & (x "/\" z) "\/" (z "/\" y) <= z "/\" (x "\/" y) ) by Th6;
then ((x "/\" z) "\/" (x "/\" y)) "\/" ((x "/\" z) "\/" (z "/\" y)) <= (x "/\" (z "\/" y)) "\/" (z "/\" (x "\/" y)) by 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;
hence ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) <= (x "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" (z "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) by A16, A18, LATTICE3:14; :: thesis: verum

end;

A24: ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) <= (z "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" (y "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)))

proof

( (z "/\" y) "\/" (z "/\" x) <= z "/\" (y "\/" x) & (z "/\" y) "\/" (y "/\" x) <= y "/\" (z "\/" x) ) by Th6;
then ((z "/\" y) "\/" (z "/\" x)) "\/" ((z "/\" y) "\/" (y "/\" x)) <= (z "/\" (y "\/" x)) "\/" (y "/\" (z "\/" x)) by 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;
hence ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) <= (z "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" (y "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) by A17, A18, LATTICE3:14; :: thesis: verum

end;

A25: (x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) <= ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)

proof

( x "\/" (y "/\" z) <= (x "\/" y) "/\" (x "\/" z) & y "\/" (x "/\" z) <= (y "\/" x) "/\" (y "\/" z) ) by Th7;
then (x "\/" (y "/\" z)) "/\" (y "\/" (x "/\" z)) <= ((x "\/" y) "/\" (x "\/" z)) "/\" ((y "\/" x) "/\" (y "\/" z)) by 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 A19, A20, 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;
hence (x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) <= ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) by LATTICE3:16; :: thesis: verum

end;

A26: (x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) <= ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)

proof

( x "\/" (z "/\" y) <= (x "\/" z) "/\" (x "\/" y) & z "\/" (x "/\" y) <= (z "\/" x) "/\" (z "\/" y) ) by Th7;
then (x "\/" (z "/\" y)) "/\" (z "\/" (x "/\" y)) <= ((x "\/" z) "/\" (x "\/" y)) "/\" ((z "\/" x) "/\" (z "\/" y)) by 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 A19, A21, 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;
hence (x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) <= ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) by LATTICE3:16; :: thesis: verum

end;

A27: (z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) <= ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)

proof

( z "\/" (y "/\" x) <= (z "\/" y) "/\" (z "\/" x) & y "\/" (z "/\" x) <= (y "\/" z) "/\" (y "\/" x) ) by Th7;
then (z "\/" (y "/\" x)) "/\" (y "\/" (z "/\" x)) <= ((z "\/" y) "/\" (z "\/" x)) "/\" ((y "\/" z) "/\" (y "\/" x)) by 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 A20, A21, 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;
hence (z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) <= ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) by LATTICE3:16; :: thesis: verum

end;

( x "/\" (y "\/" z) <= x & x <= x "\/" z ) by YELLOW_0:22, YELLOW_0:23;
then A28: x "/\" (y "\/" z) <= x "\/" z by YELLOW_0:def 2;
( x "/\" (z "\/" y) <= x & x <= x "\/" y ) by YELLOW_0:22, YELLOW_0:23;
then A29: x "/\" (z "\/" y) <= x "\/" y by YELLOW_0:def 2;
( z "/\" (y "\/" x) <= z & z <= z "\/" x ) by YELLOW_0:22, YELLOW_0:23;
then A30: z "/\" (y "\/" x) <= z "\/" x by YELLOW_0:def 2;
( x "/\" z <= x & x <= x "\/" (y "/\" z) ) by YELLOW_0:22, YELLOW_0:23;
then A31: x "/\" z <= x "\/" (y "/\" z) by YELLOW_0:def 2;
( x "/\" y <= x & x <= x "\/" (z "/\" y) ) by YELLOW_0:22, YELLOW_0:23;
then A32: x "/\" y <= x "\/" (z "/\" y) by YELLOW_0:def 2;
( z "/\" x <= z & z <= z "\/" (y "/\" x) ) by YELLOW_0:22, YELLOW_0:23;
then A33: z "/\" x <= z "\/" (y "/\" x) by YELLOW_0:def 2;
A34: y <= y "\/" z by YELLOW_0:22;
A35: z <= z "\/" y by YELLOW_0:22;
A36: y <= y "\/" x by YELLOW_0:22;
A37: y "/\" z <= y by YELLOW_0:23;
A38: z "/\" y <= z by YELLOW_0:23;
A39: y "/\" x <= y by YELLOW_0:23;
A40: (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, A5, Def3;
A41: (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, A5, Def3;
A42: ((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, A5, A40, 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 A16, A17, A22, YELLOW_5:8
.= (y "\/" (x "/\" (y "\/" z))) "/\" (x "\/" z) by A1, A28, Def3
.= ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) by A1, A34, Def3 ;
A43: ((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 A19, A20, A25, YELLOW_5:10
.= (y "/\" (x "\/" (y "/\" z))) "\/" (x "/\" z) by A1, A31, Def3
.= ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) by A1, A37, Def3 ;
A44: ((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, A5, A41, 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 A16, A18, A23, YELLOW_5:8
.= (z "\/" (x "/\" (z "\/" y))) "/\" (x "\/" y) by A1, A29, Def3
.= ((z "\/" x) "/\" (z "\/" y)) "/\" (x "\/" y) by A1, A35, Def3
.= ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) by LATTICE3:16 ;
A45: ((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 A19, A21, A26, YELLOW_5:10
.= (z "/\" (x "\/" (z "/\" y))) "\/" (x "/\" y) by A1, A32, Def3
.= ((z "/\" x) "\/" (z "/\" y)) "\/" (x "/\" y) by A1, A38, Def3
.= ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) by LATTICE3:14 ;
A46: ((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, A5, A40, 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 A17, A18, A24, YELLOW_5:8
.= (y "\/" (z "/\" (y "\/" x))) "/\" (z "\/" x) by A1, A30, Def3
.= ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) by A1, A36, Def3 ;
A47: ((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 A20, A21, A27, YELLOW_5:10
.= (y "/\" (z "\/" (y "/\" x))) "\/" (z "/\" x) by A1, A33, Def3
.= ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) by A1, A39, Def3 ;
((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) <= (x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) by A43, YELLOW_0:23;
then A48: (((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;
((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) <= (y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) by A43, 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:8;
((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) <= (z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) by A45, YELLOW_0:23;
then A50: (((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 "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) <= ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) by YELLOW_0:23;
then A51: (((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;
(y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) <= ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) by YELLOW_0:23;
then A52: (((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;
(z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) <= ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) by YELLOW_0:23;
then A53: (((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;
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 A15, A42, A44, A47, A49, A50, 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 A15, A42, A45, A46, A48, A50, 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 A15, A43, A44, A46, A48, A49, 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 A15; :: 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 )
thus 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 )

proof

now

assume x1 = y1 ; :: thesis: contradiction
then ( x1 "/\" y1 = x1 & x1 "\/" y1 = x1 ) by YELLOW_5:1, YELLOW_5:2;
hence contradiction by A15, A42, A43; :: thesis: verum

end;

hence x1 <> y1 ; :: thesis: verum

end;

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

proof

now

assume x1 = z1 ; :: thesis: contradiction
then ( x1 "/\" z1 = x1 & x1 "\/" z1 = x1 ) by YELLOW_5:1, YELLOW_5:2;
hence contradiction by A15, A44, A45; :: thesis: verum

end;

hence x1 <> z1 ; :: thesis: verum

end;

thus x1 <> t by A15, A43, A45, A46, A52, A53, 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 )
thus 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 )

proof

now

assume y1 = z1 ; :: thesis: contradiction
then ( y1 "/\" z1 = y1 & y1 "\/" z1 = y1 ) by YELLOW_5:1, YELLOW_5:2;
hence contradiction by A15, A46, A47; :: thesis: verum

end;

hence y1 <> z1 ; :: thesis: verum

end;

thus y1 <> t by A15, A43, A44, A47, A51, A53, 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 A15, A42, A45, A47, A51, A52, 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 )
thus b "/\" x1 = b :: 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 )

proof

b <= x1 by A43, YELLOW_0:23;
hence b "/\" x1 = b by YELLOW_5:10; :: thesis: verum

end;

thus b "/\" y1 = b :: 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 )

proof

b <= y1 by A43, YELLOW_0:23;
hence b "/\" y1 = b by YELLOW_5:10; :: thesis: verum

end;

thus b "/\" z1 = b :: 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 )

proof

b <= z1 by A45, YELLOW_0:23;
hence b "/\" z1 = b by YELLOW_5:10; :: thesis: verum

end;

thus x1 "/\" t = x1 :: 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 )

proof

x1 <= t by A42, YELLOW_0:22;
hence x1 "/\" t = x1 by YELLOW_5:10; :: thesis: verum

end;

thus y1 "/\" t = y1 :: thesis: ( z1 "/\" t = z1 & x1 "/\" y1 = b & x1 "/\" z1 = b & y1 "/\" z1 = b & x1 "\/" y1 = t & x1 "\/" z1 = t & y1 "\/" z1 = t )

proof

y1 <= t by A42, YELLOW_0:22;
hence y1 "/\" t = y1 by YELLOW_5:10; :: thesis: verum

end;

thus z1 "/\" t = z1 :: thesis: ( x1 "/\" y1 = b & x1 "/\" z1 = b & y1 "/\" z1 = b & x1 "\/" y1 = t & x1 "\/" z1 = t & y1 "\/" z1 = t )

proof

z1 <= t by A44, YELLOW_0:22;
hence z1 "/\" t = z1 by YELLOW_5:10; :: thesis: verum

end;

thus x1 "/\" y1 = b by A43; :: thesis: ( x1 "/\" z1 = b & y1 "/\" z1 = b & x1 "\/" y1 = t & x1 "\/" z1 = t & y1 "\/" z1 = t )
thus x1 "/\" z1 = b by A45; :: thesis: ( y1 "/\" z1 = b & x1 "\/" y1 = t & x1 "\/" z1 = t & y1 "\/" z1 = t )
thus y1 "/\" z1 = b by A47; :: thesis: ( x1 "\/" y1 = t & x1 "\/" z1 = t & y1 "\/" z1 = t )
thus x1 "\/" y1 = t by A42; :: thesis: ( x1 "\/" z1 = t & y1 "\/" z1 = t )
thus x1 "\/" z1 = t by A44; :: thesis: y1 "\/" z1 = t
thus y1 "\/" z1 = t by A46; :: 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