let L be LATTICE; ( L is modular implies ( L is distributive 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 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
; ( L is distributive 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 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 ( ex a, b, c, d, e being Element of L st
( a <> d & d "/\" e = d & b "/\" c = a & b "/\" d = a & c "/\" d = a & b "\/" c = e ) implies not L is distributive )given a,
b,
c,
d,
e being
Element of
L such that A2:
a <> d
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
;
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;
verum end;
hence
( L is distributive implies for a, b, c, d, e being Element of L holds
( not a,b,c,d,e are_mutually_distinct or not a "/\" b = a or not a "/\" c = a or not 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 ) )
; ( ( 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 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 ( not L is distributive 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 & 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 ) )assume
not
L is
distributive
;
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 & 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)
;
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;
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
.=
((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)
by A1, A36
;
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
.=
((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)
by A1, A55
;
(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;
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
.=
(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
.=
((z "\/" x) "/\" (z "\/" y)) "/\" (x "\/" y)
by A1, A33
.=
((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;
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
.=
(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
.=
((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)
by A1, A25
;
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
.=
(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
.=
((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)
by A1, A44
;
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
.=
((z "/\" x) "\/" (z "/\" y)) "\/" (x "/\" y)
by A1, A63
.=
((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,
c,
d,
e are_mutually_distinct &
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 )
verumproof
take
((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)
;
ex b, c, d, e being Element of L st
( ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x),b,c,d,e are_mutually_distinct & (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)) "/\" b = ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) & (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)) "/\" c = ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) & (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)) "/\" d = ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) & b "/\" e = b & c "/\" e = c & d "/\" e = d & b "/\" c = ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) & b "/\" d = ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) & c "/\" d = ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) & b "\/" c = e & b "\/" d = e & c "\/" d = e )
take
(x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))
;
ex c, d, e being Element of L st
( ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x),(x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)),c,d,e are_mutually_distinct & (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)) "/\" ((x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) = ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) & (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)) "/\" c = ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) & (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)) "/\" d = ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) & ((x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "/\" e = (x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) & c "/\" e = c & d "/\" e = d & ((x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "/\" c = ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) & ((x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "/\" d = ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) & c "/\" d = ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) & ((x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" c = e & ((x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" d = e & c "\/" d = e )
take
(y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))
;
ex d, e being Element of L st
( ((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)),d,e are_mutually_distinct & (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)) "/\" ((x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" 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))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) = ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) & (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)) "/\" d = ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) & ((x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "/\" e = (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))) "/\" e = (y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) & d "/\" e = d & ((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 "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) & ((x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "/\" d = ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) & ((y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "/\" d = ((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))) = e & ((x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" d = e & ((y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" d = e )
take
(z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))
;
ex e being Element of L st
( ((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)),(z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)),e are_mutually_distinct & (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)) "/\" ((x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" 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))) "/\" (((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))) "/\" (((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))) "/\" e = (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))) "/\" e = (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))) "/\" e = (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))) "/\" ((y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" 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))) "/\" ((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))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "/\" ((z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" 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))) "\/" ((y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) = e & ((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))) = e & ((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))) = e )
take
((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)),(z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)),((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) are_mutually_distinct & (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)) "/\" ((x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" 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))) "/\" (((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))) "/\" (((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))) "/\" (((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))) "/\" (((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))) "/\" (((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))) "/\" ((y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" 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))) "/\" ((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))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "/\" ((z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" 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))) "\/" ((y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" 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))) "\/" ((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))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" ((z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) = ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) )
thus
((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) <> (x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))
by A14, A68, A66, A60, A57, A71, YELLOW_5:2;
ZFMISC_1:def 7 ( not ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) = (y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) & not ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) = (z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) & not ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) = ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) & not (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)) & not (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)) & not (x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) = ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) & not (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)) & not (y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) = ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) & not (z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" 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))) = ((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 "/\" 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 "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) & ((x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" 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)) & ((y "\/" (((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))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) & ((z "\/" (((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))) "/\" (((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))) = ((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))) = ((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))) = ((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))) = ((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))) = ((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))) = ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) )
thus
((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) <> (y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))
by A14, A68, A70, A69, A72, A71, YELLOW_5:2;
( not ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) = (z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) & not ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) = ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) & not (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)) & not (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)) & not (x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) = ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) & not (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)) & not (y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) = ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) & not (z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" 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))) = ((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 "/\" 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 "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) & ((x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" 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)) & ((y "\/" (((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))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) & ((z "\/" (((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))) "/\" (((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))) = ((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))) = ((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))) = ((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))) = ((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))) = ((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))) = ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) )
thus
((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) <> (z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))
by A14, A56, A66, A69, A72, A57, YELLOW_5:2;
( not ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) = ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) & not (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)) & not (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)) & not (x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) = ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) & not (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)) & not (y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) = ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) & not (z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" 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))) = ((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 "/\" 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 "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) & ((x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" 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)) & ((y "\/" (((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))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) & ((z "\/" (((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))) "/\" (((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))) = ((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))) = ((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))) = ((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))) = ((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))) = ((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))) = ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) )
thus
((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) <> ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)
by A14;
( not (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)) & not (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)) & not (x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) = ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) & not (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)) & not (y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) = ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) & not (z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" 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))) = ((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 "/\" 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 "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) & ((x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" 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)) & ((y "\/" (((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))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) & ((z "\/" (((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))) "/\" (((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))) = ((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))) = ((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))) = ((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))) = ((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))) = ((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))) = ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) )
hence
(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))
;
( not (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)) & not (x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) = ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) & not (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)) & not (y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) = ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) & not (z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" 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))) = ((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 "/\" 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 "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) & ((x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" 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)) & ((y "\/" (((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))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) & ((z "\/" (((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))) "/\" (((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))) = ((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))) = ((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))) = ((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))) = ((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))) = ((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))) = ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) )
hence
(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))
;
( not (x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) = ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) & not (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)) & not (y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) = ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) & not (z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" 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))) = ((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 "/\" 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 "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) & ((x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" 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)) & ((y "\/" (((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))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) & ((z "\/" (((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))) "/\" (((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))) = ((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))) = ((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))) = ((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))) = ((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))) = ((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))) = ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) )
thus
(x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) <> ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)
by A14, A56, A70, A69, A49, A41, YELLOW_5:1;
( not (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)) & not (y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) = ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) & not (z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" 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))) = ((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 "/\" 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 "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) & ((x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" 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)) & ((y "\/" (((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))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) & ((z "\/" (((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))) "/\" (((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))) = ((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))) = ((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))) = ((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))) = ((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))) = ((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))) = ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) )
hence
(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))
;
( not (y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) = ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) & not (z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" 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))) = ((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 "/\" 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 "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) & ((x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" 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)) & ((y "\/" (((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))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) & ((z "\/" (((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))) "/\" (((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))) = ((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))) = ((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))) = ((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))) = ((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))) = ((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))) = ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) )
thus
(y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) <> ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)
by A14, A56, A66, A60, A59, A41, YELLOW_5:1;
( not (z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" 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))) = ((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 "/\" 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 "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x) & ((x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" 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)) & ((y "\/" (((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))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) & ((z "\/" (((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))) "/\" (((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))) = ((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))) = ((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))) = ((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))) = ((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))) = ((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))) = ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) )
thus
(z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) <> ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)
by A14, A68, A70, A60, A59, A49, YELLOW_5:1;
( (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)) "/\" ((x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" 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))) "/\" (((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))) "/\" (((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))) "/\" (((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))) "/\" (((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))) "/\" (((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))) "/\" ((y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" 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))) "/\" ((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))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "/\" ((z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" 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))) "\/" ((y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" 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))) "\/" ((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))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" ((z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" 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 A56, YELLOW_0:23;
hence
(((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)) "/\" ((x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) = ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)
by YELLOW_5:10;
( (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)) "/\" ((y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" 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))) "/\" (((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))) "/\" (((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))) "/\" (((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))) "/\" (((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))) "/\" ((y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" 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))) "/\" ((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))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "/\" ((z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" 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))) "\/" ((y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" 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))) "\/" ((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))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" ((z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" 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))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))
by A56, YELLOW_0:23;
hence
(((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)) "/\" ((y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) = ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)
by YELLOW_5:10;
( (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)) "/\" ((z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" 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))) "/\" (((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))) "/\" (((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))) "/\" (((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))) "/\" ((y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" 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))) "/\" ((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))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "/\" ((z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" 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))) "\/" ((y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" 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))) "\/" ((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))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" ((z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" 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))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))
by A70, YELLOW_0:23;
hence
(((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)) "/\" ((z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) = ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)
by YELLOW_5:10;
( ((x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" 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)) & ((y "\/" (((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))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) & ((z "\/" (((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))) "/\" (((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))) = ((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))) = ((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))) = ((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))) = ((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))) = ((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))) = ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) )
(x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) <= ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)
by A68, YELLOW_0:22;
hence
((x "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" 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)) = (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))) "/\" (((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))) "/\" ((y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" 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))) "/\" ((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))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "/\" ((z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" 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))) "\/" ((y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" 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))) "\/" ((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))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" ((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))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) <= ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)
by A68, YELLOW_0:22;
hence
((y "\/" (((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))) "/\" (((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)) = (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))) "/\" ((y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" 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))) "/\" ((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))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "/\" ((z "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" 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))) "\/" ((y "\/" (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" 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))) "\/" ((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))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))) "\/" ((z "\/" (((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))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) <= ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)
by A66, YELLOW_0:22;
hence
((z "\/" (((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))) "/\" (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x))
by YELLOW_5:10;
( ((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 "/\" 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))) = ((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))) = ((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))) = ((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))) = ((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))) = ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) )
thus
((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 "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)
by A56;
( ((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 "/\" 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))) = ((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))) = ((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))) = ((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))) = ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) )
thus
((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 "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)
by A70;
( ((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))) = ((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))) = ((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))) = ((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))) = ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) )
thus
((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))) = ((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)
by A60;
( ((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 "\/" 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))) = ((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))) = ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) )
thus
((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 "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)
by A68;
( ((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 "\/" 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))) = ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x) )
thus
((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 "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)
by A66;
((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))) = ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)
thus
((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))) = ((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)
by A69;
verum
end; end;
hence
( ( for a, b, c, d, e being Element of L holds
( not a,b,c,d,e are_mutually_distinct or not a "/\" b = a or not a "/\" c = a or not 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 )
; verum