let x, y, z be ext-real number ; :: 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 ) and
A2: ( not x = -infty or not y = -infty ) and
A3: ( not y = +infty or not z = +infty ) and
A4: ( not y = -infty or not z = -infty ) and
A5: ( not x = +infty or not z = -infty ) and
A6: ( not x = -infty or not z = +infty ) ; :: thesis: (x - y) + z = x - (y - z)

per cases ( x = +infty or x = -infty or ( x <> +infty & x <> -infty ) ) ;

suppose A7: x = +infty ; :: thesis: (x - y) + z = x - (y - z)

then x - y = +infty by A1, Th16;
then A8: (x - y) + z = +infty by A5, A7, Def3;
y - z <> +infty by A1, A5, A7, Th32;
hence (x - y) + z = x - (y - z) by A7, A8, Th16; :: thesis: verum

end;

suppose A9: x = -infty ; :: thesis: (x - y) + z = x - (y - z)

then x - y = -infty by A2, Th29;
then A10: (x - y) + z = -infty by A6, A9, Def3;
y - z <> -infty by A2, A6, A9, Th33;
hence (x - y) + z = x - (y - z) by A9, A10, Th29; :: thesis: verum

end;

suppose A11: ( x <> +infty & x <> -infty ) ; :: thesis: (x - y) + z = x - (y - z)

then x in REAL by XXREAL_0:14;
then reconsider a = x as real number ;

per cases ( y = +infty or y = -infty or ( y <> +infty & y <> -infty ) ) ;

suppose A12: y = +infty ; :: thesis: (x - y) + z = x - (y - z)

then ( x - y = -infty & y - z = +infty ) by A3, A11, Th16;
hence (x - y) + z = x - (y - z) by A3, A12, Def3; :: thesis: verum

end;

suppose A13: y = -infty ; :: thesis: (x - y) + z = x - (y - z)

then ( x - y = +infty & y - z = -infty ) by A4, A11, Th29;
hence (x - y) + z = x - (y - z) by A4, A13, Def3; :: thesis: verum

end;

suppose ( y <> +infty & y <> -infty ) ; :: thesis: (x - y) + z = x - (y - z)

then y in REAL by XXREAL_0:14;
then reconsider b = y as real number ;
A14: x - y = a - b ;

per cases ( z = +infty or z = -infty or ( z <> +infty & z <> -infty ) ) ;

suppose z = +infty ; :: thesis: (x - y) + z = x - (y - z)

then ( (x - y) + z = +infty & y - z = -infty ) by A14, Th16, Def3;
hence (x - y) + z = x - (y - z) by A11, Th29; :: thesis: verum

end;

suppose z = -infty ; :: thesis: (x - y) + z = x - (y - z)

then ( (x - y) + z = -infty & y - z = +infty ) by A14, Th29, Def3;
hence (x - y) + z = x - (y - z) by A11, Th16; :: thesis: verum

end;

suppose ( z <> +infty & z <> -infty ) ; :: thesis: (x - y) + z = x - (y - z)

then z in REAL by XXREAL_0:14;
then reconsider c = z as real number ;
A15: ( (x - y) + z = (a - b) + c & y - z = b - c ) ;
x - (y - z) = a - (b - c) ;
hence (x - y) + z = x - (y - z) by A15; :: thesis: verum

end;

end;

end;

end;

end;

end;