Theorem GT-1. Groups satisfy the quotient condition. Let a, b, c, d, a_{0}, b_{0}, c_{0}, d_{0} be constants.

\{ \begin{matrix}GT \\ aa_{0} = bb_{0} \\ ca_{0} = db_{0} \\ ac_{0} = bd_{0} \end{matrix} \} ⇒ \{cc_{0} = dd_{0}\}.

Proof (found by Otter 3.0.4 on gyro at 0.35 seconds).

1 d · d_{0} ≠ c · c_{0} 4,3 (x · y) · z = x · (y · z) 15 x′ · (x · y) = y 18,17 x · (x′ · y) = y 23 a · a_{0} = b · b_{0}

24 b · b_{0} = a · a_{0} [flip 23]

26 c · a_{0} = d · b_{0}

27 d · b_{0} = c · a_{0} [flip 26]

29 a · c_{0} = b · d_{0}

30  b · d_{0} = a · c_{0}  [flip 29]
32  b · (b_{0} · x) = a · (a_{0} · x)  [24 → 3 :4, flip]
34  d · (b_{0} · x) = c · (a_{0} · x)  [27 → 3 :4, flip]
44  b′ · (a · c_{0}) = d_{0}  [30 → 15]
62  b′ · (a · (a_{0} · x)) = b_{0} · x  [32 → 15]
97,96  b′ · (a · x) = b_{0} · (a_{0}′ · x)  [17 → 62]
106  b_{0} · (a_{0}′ · c_{0}) = d_{0}  [44 :97]
114  d · d_{0} = c · c_{0}  [106 → 34 :18]
116  □  [114,1]