let x, y, z, t be positive Nat; :: thesis: ( x <= y & y <= z & z <= t implies ( (((1 / x) + (1 / y)) + (1 / z)) + (1 / t) = 1 iff ( ( x = 2 & y = 3 & z = 7 & t = 42 ) or ( x = 2 & y = 3 & z = 8 & t = 24 ) or ( x = 2 & y = 3 & z = 9 & t = 18 ) or ( x = 2 & y = 3 & z = 10 & t = 15 ) or ( x = 2 & y = 3 & z = 12 & t = 12 ) or ( x = 2 & y = 4 & z = 5 & t = 20 ) or ( x = 2 & y = 4 & z = 6 & t = 12 ) or ( x = 2 & y = 4 & z = 8 & t = 8 ) or ( x = 2 & y = 5 & z = 5 & t = 10 ) or ( x = 2 & y = 6 & z = 6 & t = 6 ) or ( x = 3 & y = 3 & z = 4 & t = 12 ) or ( x = 3 & y = 3 & z = 6 & t = 6 ) or ( x = 3 & y = 4 & z = 4 & t = 6 ) or ( x = 4 & y = 4 & z = 4 & t = 4 ) ) ) )
assume that
A1: x <= y and
A2: y <= z and
A3: z <= t ; :: thesis: ( (((1 / x) + (1 / y)) + (1 / z)) + (1 / t) = 1 iff ( ( x = 2 & y = 3 & z = 7 & t = 42 ) or ( x = 2 & y = 3 & z = 8 & t = 24 ) or ( x = 2 & y = 3 & z = 9 & t = 18 ) or ( x = 2 & y = 3 & z = 10 & t = 15 ) or ( x = 2 & y = 3 & z = 12 & t = 12 ) or ( x = 2 & y = 4 & z = 5 & t = 20 ) or ( x = 2 & y = 4 & z = 6 & t = 12 ) or ( x = 2 & y = 4 & z = 8 & t = 8 ) or ( x = 2 & y = 5 & z = 5 & t = 10 ) or ( x = 2 & y = 6 & z = 6 & t = 6 ) or ( x = 3 & y = 3 & z = 4 & t = 12 ) or ( x = 3 & y = 3 & z = 6 & t = 6 ) or ( x = 3 & y = 4 & z = 4 & t = 6 ) or ( x = 4 & y = 4 & z = 4 & t = 4 ) ) )
thus ( not (((1 / x) + (1 / y)) + (1 / z)) + (1 / t) = 1 or ( x = 2 & y = 3 & z = 7 & t = 42 ) or ( x = 2 & y = 3 & z = 8 & t = 24 ) or ( x = 2 & y = 3 & z = 9 & t = 18 ) or ( x = 2 & y = 3 & z = 10 & t = 15 ) or ( x = 2 & y = 3 & z = 12 & t = 12 ) or ( x = 2 & y = 4 & z = 5 & t = 20 ) or ( x = 2 & y = 4 & z = 6 & t = 12 ) or ( x = 2 & y = 4 & z = 8 & t = 8 ) or ( x = 2 & y = 5 & z = 5 & t = 10 ) or ( x = 2 & y = 6 & z = 6 & t = 6 ) or ( x = 3 & y = 3 & z = 4 & t = 12 ) or ( x = 3 & y = 3 & z = 6 & t = 6 ) or ( x = 3 & y = 4 & z = 4 & t = 6 ) or ( x = 4 & y = 4 & z = 4 & t = 4 ) ) :: thesis: ( ( ( x = 2 & y = 3 & z = 7 & t = 42 ) or ( x = 2 & y = 3 & z = 8 & t = 24 ) or ( x = 2 & y = 3 & z = 9 & t = 18 ) or ( x = 2 & y = 3 & z = 10 & t = 15 ) or ( x = 2 & y = 3 & z = 12 & t = 12 ) or ( x = 2 & y = 4 & z = 5 & t = 20 ) or ( x = 2 & y = 4 & z = 6 & t = 12 ) or ( x = 2 & y = 4 & z = 8 & t = 8 ) or ( x = 2 & y = 5 & z = 5 & t = 10 ) or ( x = 2 & y = 6 & z = 6 & t = 6 ) or ( x = 3 & y = 3 & z = 4 & t = 12 ) or ( x = 3 & y = 3 & z = 6 & t = 6 ) or ( x = 3 & y = 4 & z = 4 & t = 6 ) or ( x = 4 & y = 4 & z = 4 & t = 4 ) ) implies (((1 / x) + (1 / y)) + (1 / z)) + (1 / t) = 1 )

proof

assume A4: (((1 / x) + (1 / y)) + (1 / z)) + (1 / t) = 1 ; :: thesis: ( ( x = 2 & y = 3 & z = 7 & t = 42 ) or ( x = 2 & y = 3 & z = 8 & t = 24 ) or ( x = 2 & y = 3 & z = 9 & t = 18 ) or ( x = 2 & y = 3 & z = 10 & t = 15 ) or ( x = 2 & y = 3 & z = 12 & t = 12 ) or ( x = 2 & y = 4 & z = 5 & t = 20 ) or ( x = 2 & y = 4 & z = 6 & t = 12 ) or ( x = 2 & y = 4 & z = 8 & t = 8 ) or ( x = 2 & y = 5 & z = 5 & t = 10 ) or ( x = 2 & y = 6 & z = 6 & t = 6 ) or ( x = 3 & y = 3 & z = 4 & t = 12 ) or ( x = 3 & y = 3 & z = 6 & t = 6 ) or ( x = 3 & y = 4 & z = 4 & t = 6 ) or ( x = 4 & y = 4 & z = 4 & t = 4 ) )

A5: now :: thesis: not x < 2

A6: ((1 / y) + (1 / z)) + (1 / t) > 0 ;
assume x < 2 ; :: thesis: contradiction
then ((((1 / 1) + (1 / y)) + (1 / z)) + (1 / t)) - 1 = 1 - 1 by A4, NAT_1:23;
hence contradiction by A6; :: thesis: verum

end;

A7: now :: thesis: ( y > 4 implies ((1 / y) + (1 / z)) + (1 / t) <= (2 / 5) + (1 / 5) )

assume y > 4 ; :: thesis: ((1 / y) + (1 / z)) + (1 / t) <= (2 / 5) + (1 / 5)
then A8: y >= 4 + 1 by NAT_1:13;
then A9: 1 / y <= 1 / 5 by XREAL_1:118;
A10: z >= 5 by A2, A8, XXREAL_0:2;
then 1 / z <= 1 / 5 by XREAL_1:118;
then A11: (1 / y) + (1 / z) <= (1 / 5) + (1 / 5) by A9, XREAL_1:7;
t >= 5 by A3, A10, XXREAL_0:2;
then 1 / t <= 1 / 5 by XREAL_1:118;
hence ((1 / y) + (1 / z)) + (1 / t) <= (2 / 5) + (1 / 5) by A11, XREAL_1:7; :: thesis: verum

end;

now :: thesis: ( ( x = 2 & ( ( y = 2 & contradiction ) or ( y = 3 & ( ( z = 7 & x = 2 & y = 3 & z = 7 & t = 42 ) or ( z = 8 & x = 2 & y = 3 & z = 8 & t = 24 ) or ( z = 9 & x = 2 & y = 3 & z = 9 & t = 18 ) or ( z = 10 & x = 2 & y = 3 & z = 10 & t = 15 ) or ( z = 11 & contradiction ) or ( z = 12 & x = 2 & y = 3 & z = 12 & t = 12 ) ) ) or ( y = 4 & ( ( z = 5 & x = 2 & y = 4 & z = 5 & t = 20 ) or ( z = 6 & x = 2 & y = 4 & z = 6 & t = 12 ) or ( z = 7 & contradiction ) or ( z = 8 & x = 2 & y = 4 & z = 8 & t = 8 ) ) ) or ( y = 5 & ( ( z = 5 & x = 2 & y = 5 & z = 5 & t = 10 ) or ( z = 6 & contradiction ) ) ) or ( y = 6 & x = 2 & y = 6 & z = 6 & t = 6 ) ) ) or ( x = 3 & ( ( y = 3 & ( ( z = 3 & contradiction ) or ( z = 4 & x = 3 & y = 3 & z = 4 & t = 12 ) or ( z = 5 & contradiction ) or ( z = 6 & x = 3 & y = 3 & z = 6 & t = 6 ) ) ) or ( y = 4 & x = 3 & y = 4 & z = 4 & t = 6 ) ) ) or ( x = 4 & x = 4 & y = 4 & z = 4 & t = 4 ) )

A12: not ((2 * 7) + 1) / 2 is integer by NUMBER05:37;
A13: (1 / z) + 0 < (1 / z) + (1 / t) by XREAL_1:8;

now :: thesis: not x > 4

assume A14: x > 4 ; :: thesis: contradiction
then 1 / x < 1 / 4 by XREAL_1:76;
then (1 / x) + (((1 / y) + (1 / z)) + (1 / t)) < (1 / 4) + (3 / 5) by A1, A7, A14, XXREAL_0:2, XREAL_1:8;
hence contradiction by A4; :: thesis: verum

end;

then not not x = 0 & ... & not x = 4 ;

per cases then ( x = 2 or x = 3 or x = 4 ) by A5;

case A15: x = 2 ; :: thesis: verum

then A16: ((((1 / 2) + (1 / y)) + (1 / z)) + (1 / t)) - (1 / 2) = 1 - (1 / 2) by A4;
then A17: ((1 / y) + (1 / z)) + (1 / t) = 1 / 2 ;
1 / z <= 1 / y by A2, XREAL_1:118;
then A18: (1 / y) + (1 / z) <= (1 / y) + (1 / y) by XREAL_1:7;
1 / t <= 1 / z by A3, XREAL_1:118;
then A19: (1 / z) + (1 / t) <= (1 / z) + (1 / z) by XREAL_1:7;
y <= t by A2, A3, XXREAL_0:2;
then 1 / t <= 1 / y by XREAL_1:118;
then ((1 / y) + (1 / z)) + (1 / t) <= ((1 / y) + (1 / y)) + (1 / y) by A18, XREAL_1:7;
then (1 / 2) * y <= (3 / y) * y by A16, XREAL_1:64;
then (1 / 2) * y <= 3 by XCMPLX_1:87;
then ((1 / 2) * y) * 2 <= 3 * 2 by XREAL_1:64;
then not not y = 0 & ... & not y = 6 ;

per cases then ( y = 2 or y = 3 or y = 4 or y = 5 or y = 6 ) by A1, A15;

case y = 2 ; :: thesis: contradiction

then A20: ((1 / 2) + (1 / z)) + (1 / t) = 1 / 2 by A17;
(1 / z) + (1 / t) > 0 ;
hence contradiction by A20; :: thesis: verum

end;

case A21: y = 3 ; :: thesis: verum

then A22: (((1 / 3) + (1 / z)) + (1 / t)) - (1 / 3) = (1 / 2) - (1 / 3) by A16;
then (1 / 6) * z <= (2 / z) * z by A19, XREAL_1:64;
then (1 / 6) * z <= 2 by XCMPLX_1:87;
then ((1 / 6) * z) * 6 <= 2 * 6 by XREAL_1:64;
then not not z = 0 & ... & not z = 12 ;

per cases then ( z = 7 or z = 8 or z = 9 or z = 10 or z = 11 or z = 12 ) by A13, A22;

case A23: z = 7 ; :: thesis: ( x = 2 & y = 3 & z = 7 & t = 42 )

then ((1 / 7) + (1 / t)) - (1 / 7) = (1 / 6) - (1 / 7) by A22;
then 1 / t = 1 / 42 ;
hence ( x = 2 & y = 3 & z = 7 & t = 42 ) by A15, A21, A23, XCMPLX_1:59; :: thesis: verum

end;

case A24: z = 8 ; :: thesis: ( x = 2 & y = 3 & z = 8 & t = 24 )

then ((1 / 8) + (1 / t)) - (1 / 8) = (1 / 6) - (1 / 8) by A22;
then 1 / t = 1 / 24 ;
hence ( x = 2 & y = 3 & z = 8 & t = 24 ) by A15, A21, A24, XCMPLX_1:59; :: thesis: verum

end;

case A25: z = 9 ; :: thesis: ( x = 2 & y = 3 & z = 9 & t = 18 )

then ((1 / 9) + (1 / t)) - (1 / 9) = (1 / 6) - (1 / 9) by A22;
then 1 / t = 1 / 18 ;
hence ( x = 2 & y = 3 & z = 9 & t = 18 ) by A15, A21, A25, XCMPLX_1:59; :: thesis: verum

end;

case A26: z = 10 ; :: thesis: ( x = 2 & y = 3 & z = 10 & t = 15 )

then ((1 / 10) + (1 / t)) - (1 / 10) = (1 / 6) - (1 / 10) by A22;
then 1 / t = 1 / 15 ;
hence ( x = 2 & y = 3 & z = 10 & t = 15 ) by A15, A21, A26, XCMPLX_1:59; :: thesis: verum

end;

case z = 11 ; :: thesis: contradiction

then ((1 / 11) + (1 / t)) - (1 / 11) = (1 / 6) - (1 / 11) by A22;
then (1 / t) " = (5 / 66) " ;
then t = ((5 * 13) + 1) / 5 ;
hence contradiction by NUMBER05:37; :: thesis: verum

end;

case A27: z = 12 ; :: thesis: ( x = 2 & y = 3 & z = 12 & t = 12 )

then ((1 / 12) + (1 / t)) - (1 / 12) = (1 / 6) - (1 / 12) by A22;
hence ( x = 2 & y = 3 & z = 12 & t = 12 ) by A15, A21, A27, XCMPLX_1:59; :: thesis: verum

end;

end;

end;

case A28: y = 4 ; :: thesis: verum

then A29: ((1 / 4) + (1 / z)) + (1 / t) = 1 / 2 by A16;
then A30: (1 / z) + (1 / t) = 1 / 4 ;
(1 / 4) * z <= (2 / z) * z by A19, A29, XREAL_1:64;
then (1 / 4) * z <= 2 by XCMPLX_1:87;
then ((1 / 4) * z) * 4 <= 2 * 4 by XREAL_1:64;
then not not z = 0 & ... & not z = 8 ;

per cases then ( z = 5 or z = 6 or z = 7 or z = 8 ) by A29, A13;

case A31: z = 5 ; :: thesis: ( x = 2 & y = 4 & z = 5 & t = 20 )

then ((1 / 5) + (1 / t)) - (1 / 5) = (1 / 4) - (1 / 5) by A30;
then 1 / t = 1 / 20 ;
hence ( x = 2 & y = 4 & z = 5 & t = 20 ) by A15, A28, A31, XCMPLX_1:59; :: thesis: verum

end;

case A32: z = 6 ; :: thesis: ( x = 2 & y = 4 & z = 6 & t = 12 )

then ((1 / 6) + (1 / t)) - (1 / 6) = (1 / 4) - (1 / 6) by A30;
then 1 / t = 1 / 12 ;
hence ( x = 2 & y = 4 & z = 6 & t = 12 ) by A15, A28, A32, XCMPLX_1:59; :: thesis: verum

end;

case z = 7 ; :: thesis: contradiction

then ((1 / 7) + (1 / t)) - (1 / 7) = (1 / 4) - (1 / 7) by A30;
then (1 / t) " = (3 / 28) " ;
then t = ((9 * 3) + 1) / 3 ;
hence contradiction by NUMBER05:37; :: thesis: verum

end;

case A33: z = 8 ; :: thesis: ( x = 2 & y = 4 & z = 8 & t = 8 )

then ((1 / 8) + (1 / t)) - (1 / 8) = (1 / 4) - (1 / 8) by A30;
hence ( x = 2 & y = 4 & z = 8 & t = 8 ) by A15, A28, A33, XCMPLX_1:59; :: thesis: verum

end;

end;

end;

case A34: y = 5 ; :: thesis: verum

then A35: ((1 / 5) + (1 / z)) + (1 / t) = 1 / 2 by A16;
then A36: (1 / z) + (1 / t) = 3 / 10 ;
(3 / 10) * z <= (2 / z) * z by A19, A35, XREAL_1:64;
then (3 / 10) * z <= 2 by XCMPLX_1:87;
then ((3 / 10) * z) * (10 / 3) <= 2 * (10 / 3) by XREAL_1:64;
then z < 6 + 1 by XXREAL_0:2;
then z <= 6 by NAT_1:13;
then not not z = 0 & ... & not z = 6 ;

per cases then ( z = 5 or z = 6 ) by A2, A34;

case A37: z = 5 ; :: thesis: ( x = 2 & y = 5 & z = 5 & t = 10 )

then ((1 / 5) + (1 / t)) - (1 / 5) = (3 / 10) - (1 / 5) by A36;
then 1 / t = 1 / 10 ;
hence ( x = 2 & y = 5 & z = 5 & t = 10 ) by A15, A34, A37, XCMPLX_1:59; :: thesis: verum

end;

case z = 6 ; :: thesis: contradiction

then ((1 / 6) + (1 / t)) - (1 / 6) = (3 / 10) - (1 / 6) by A36;
then (1 / t) " = (2 / 15) " ;
hence contradiction by A12; :: thesis: verum

end;

end;

end;

case A38: y = 6 ; :: thesis: ( x = 2 & y = 6 & z = 6 & t = 6 )

then A39: ((1 / 6) + (1 / z)) + (1 / t) = 1 / 2 by A16;
then A40: (1 / z) + (1 / t) = 1 / 3 ;
(1 / 3) " >= (2 / z) " by A19, A39, XREAL_1:85;
then 3 / 1 >= z / 2 by XCMPLX_1:213;
then A41: 3 * 2 >= (z / 2) * 2 by XREAL_1:64;
then (1 / 6) + (1 / t) = 1 / 3 by A2, A40, A38, XXREAL_0:1;
hence ( x = 2 & y = 6 & z = 6 & t = 6 ) by A2, A15, A38, A41, XCMPLX_1:59, XXREAL_0:1; :: thesis: verum

end;

end;

end;

case A42: x = 3 ; :: thesis: verum

then A43: ((((1 / 3) + (1 / y)) + (1 / z)) + (1 / t)) - (1 / 3) = 1 - (1 / 3) by A4;
then not not y = 0 & ... & not y = 4 by A7;

per cases then ( y = 3 or y = 4 ) by A1, A42;

case A44: y = 3 ; :: thesis: verum

then A45: (((1 / 3) + (1 / z)) + (1 / t)) - (1 / 3) = (2 / 3) - (1 / 3) by A43;
then A46: (1 / z) + (1 / t) = 1 / 3 ;

now :: thesis: not z > 6

assume A47: z > 6 ; :: thesis: contradiction
then A48: 1 / z < 1 / 6 by XREAL_1:76;
t > 6 by A3, A47, XXREAL_0:2;
then 1 / t < 1 / 6 by XREAL_1:76;
then (1 / z) + (1 / t) < (1 / 6) + (1 / 6) by A48, XREAL_1:8;
hence contradiction by A45; :: thesis: verum

end;

then not not z = 0 & ... & not z = 6 ;

per cases then ( z = 3 or z = 4 or z = 5 or z = 6 ) by A2, A44;

case z = 3 ; :: thesis: contradiction

then A49: (1 / 3) + (1 / t) = 1 / 3 by A46;
1 / t > 0 ;
hence contradiction by A49; :: thesis: verum

end;

case A50: z = 4 ; :: thesis: ( x = 3 & y = 3 & z = 4 & t = 12 )

then (1 / 4) + (1 / t) = 1 / 3 by A45;
then 1 / t = 1 / 12 ;
hence ( x = 3 & y = 3 & z = 4 & t = 12 ) by A42, A44, A50, XCMPLX_1:59; :: thesis: verum

end;

case z = 5 ; :: thesis: contradiction

then (1 / 5) + (1 / t) = 1 / 3 by A45;
then (1 / t) " = (2 / 15) " ;
hence contradiction by A12; :: thesis: verum

end;

case A51: z = 6 ; :: thesis: ( x = 3 & y = 3 & z = 6 & t = 6 )

then (1 / 6) + (1 / t) = 1 / 3 by A45;
hence ( x = 3 & y = 3 & z = 6 & t = 6 ) by A42, A44, A51, XCMPLX_1:59; :: thesis: verum

end;

end;

end;

case A52: y = 4 ; :: thesis: ( x = 3 & y = 4 & z = 4 & t = 6 )

then (((1 / 4) + (1 / z)) + (1 / t)) - (1 / 4) = (2 / 3) - (1 / 4) by A43;
then A53: (1 / z) + (1 / t) = 5 / 12 ;
1 / t <= 1 / z by A3, XREAL_1:118;
then (1 / z) + (1 / t) <= (1 / z) + (1 / z) by XREAL_1:7;
then (1 / z) + (1 / t) <= 2 / z ;
then 5 * z <= 2 * 12 by A53, XREAL_1:106;
then (5 * z) / 5 <= (2 * 12) / 5 by XREAL_1:72;
then z < 4 + 1 by XXREAL_0:2;
then A54: z <= 4 by NAT_1:13;
then ((1 / 4) + (1 / t)) - (1 / 4) = (5 / 12) - (1 / 4) by A53, A2, A52, XXREAL_0:1;
then 1 / t = 1 / 6 ;
hence ( x = 3 & y = 4 & z = 4 & t = 6 ) by A42, A54, A2, A52, XXREAL_0:1, XCMPLX_1:59; :: thesis: verum

end;

end;

end;

case A55: x = 4 ; :: thesis: ( x = 4 & y = 4 & z = 4 & t = 4 )

then A56: ((((1 / 4) + (1 / y)) + (1 / z)) + (1 / t)) - (1 / 4) = 1 - (1 / 4) by A4;

now :: thesis: not y >= 4 + 1

assume A57: y >= 4 + 1 ; :: thesis: contradiction
then A58: 1 / y <= 1 / 5 by XREAL_1:118;
A59: z >= 5 by A2, A57, XXREAL_0:2;
then 1 / z <= 1 / 5 by XREAL_1:118;
then A60: (1 / y) + (1 / z) <= (1 / 5) + (1 / 5) by A58, XREAL_1:7;
t >= 5 by A3, A59, XXREAL_0:2;
then 1 / t <= 1 / 5 by XREAL_1:118;
then ((1 / y) + (1 / z)) + (1 / t) <= ((1 / 5) + (1 / 5)) + (1 / 5) by A60, XREAL_1:7;
hence contradiction by A56; :: thesis: verum

end;

then y <= 4 by NAT_1:13;
then A61: y = 4 by A1, A55, XXREAL_0:1;
then A62: (((1 / 4) + (1 / z)) + (1 / t)) - (1 / 4) = (3 / 4) - (1 / 4) by A56;

now :: thesis: not z >= 4 + 1

assume A63: z >= 4 + 1 ; :: thesis: contradiction
then (1 / 2) - (1 / t) <= 1 / 5 by A62, XREAL_1:118;
then A64: (1 / 2) - (1 / 5) <= 1 / t by XREAL_1:12;
t >= 5 by A3, A63, XXREAL_0:2;
then 1 / t <= 1 / 5 by XREAL_1:118;
hence contradiction by A64, XXREAL_0:2; :: thesis: verum

end;

then A65: z <= 4 by NAT_1:13;
then z = 4 by A2, A61, XXREAL_0:1;
then ((1 / 4) + (1 / t)) - (1 / 4) = (1 / 2) - (1 / 4) by A62;
hence ( x = 4 & y = 4 & z = 4 & t = 4 ) by A2, A55, A61, A65, XCMPLX_1:59, XXREAL_0:1; :: thesis: verum

end;

end;

end;

hence ( ( x = 2 & y = 3 & z = 7 & t = 42 ) or ( x = 2 & y = 3 & z = 8 & t = 24 ) or ( x = 2 & y = 3 & z = 9 & t = 18 ) or ( x = 2 & y = 3 & z = 10 & t = 15 ) or ( x = 2 & y = 3 & z = 12 & t = 12 ) or ( x = 2 & y = 4 & z = 5 & t = 20 ) or ( x = 2 & y = 4 & z = 6 & t = 12 ) or ( x = 2 & y = 4 & z = 8 & t = 8 ) or ( x = 2 & y = 5 & z = 5 & t = 10 ) or ( x = 2 & y = 6 & z = 6 & t = 6 ) or ( x = 3 & y = 3 & z = 4 & t = 12 ) or ( x = 3 & y = 3 & z = 6 & t = 6 ) or ( x = 3 & y = 4 & z = 4 & t = 6 ) or ( x = 4 & y = 4 & z = 4 & t = 4 ) ) ; :: thesis: verum

end;

thus ( ( ( x = 2 & y = 3 & z = 7 & t = 42 ) or ( x = 2 & y = 3 & z = 8 & t = 24 ) or ( x = 2 & y = 3 & z = 9 & t = 18 ) or ( x = 2 & y = 3 & z = 10 & t = 15 ) or ( x = 2 & y = 3 & z = 12 & t = 12 ) or ( x = 2 & y = 4 & z = 5 & t = 20 ) or ( x = 2 & y = 4 & z = 6 & t = 12 ) or ( x = 2 & y = 4 & z = 8 & t = 8 ) or ( x = 2 & y = 5 & z = 5 & t = 10 ) or ( x = 2 & y = 6 & z = 6 & t = 6 ) or ( x = 3 & y = 3 & z = 4 & t = 12 ) or ( x = 3 & y = 3 & z = 6 & t = 6 ) or ( x = 3 & y = 4 & z = 4 & t = 6 ) or ( x = 4 & y = 4 & z = 4 & t = 4 ) ) implies (((1 / x) + (1 / y)) + (1 / z)) + (1 / t) = 1 ) ; :: thesis: verum