let x, y, z be ExtReal; :: thesis: ( ( not x = +infty or not y = -infty ) & ( not x = -infty or not y = +infty ) & ( not y = +infty or not z = +infty ) & ( not y = -infty or not z = -infty ) & ( not x = +infty or not z = +infty ) & ( not x = -infty or not z = -infty ) implies (x + y) - z = x + (y - z) )
assume that
A1: ( ( not x = +infty or not y = -infty ) & ( not x = -infty or not y = +infty ) ) and
A2: ( ( not y = +infty or not z = +infty ) & ( not y = -infty or not z = -infty ) ) and
A3: ( ( not x = +infty or not z = +infty ) & ( not x = -infty or not z = -infty ) ) ; :: thesis: (x + y) - z = x + (y - z)
A4: ( ( not x = +infty or not - z = -infty ) & ( not x = -infty or not - z = +infty ) ) by A3, Th23;
( ( not y = +infty or not - z = -infty ) & ( not y = -infty or not - z = +infty ) ) by A2, Th23;
hence (x + y) - z = x + (y - z) by A1, A4, Th29; :: thesis: verum