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, Th16;
y + z <> +infty by A1, A5, A7, LTh8;
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, Th29;
y + z <> -infty by A2, A6, A9, LTh9;
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, Def3;
hence (x - y) - z = x - (y + z) by A3, A12, Th29; :: 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, Def3;
hence (x - y) - z = x - (y + z) by A4, A13, Th16; :: 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, Th16; :: 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, Th29; :: 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;