let x, y, z be ExtReal; :: thesis: ( ( not x = +infty or not y = -infty ) & ( not x = -infty or not y = +infty ) & not ( y = +infty & z = -infty ) & not ( y = -infty & z = +infty ) & not ( x = +infty & z = -infty ) & not ( x = -infty & z = +infty ) implies (x + y) + z = x + (y + z) )
assume A1: ( not ( x = +infty & y = -infty ) & not ( x = -infty & y = +infty ) & not ( y = +infty & z = -infty ) & not ( y = -infty & z = +infty ) & not ( x = +infty & z = -infty ) & not ( x = -infty & z = +infty ) ) ; :: thesis: (x + y) + z = x + (y + z)

per cases ( ( x in REAL & y in REAL & z in REAL ) or ( x in REAL & y = +infty & z in REAL ) or ( x in REAL & y = -infty & z in REAL ) or ( x = -infty & y in REAL & z in REAL ) or ( x = +infty & y in REAL & z in REAL ) or ( x in REAL & y in REAL & z = +infty ) or ( x in REAL & y in REAL & z = -infty ) or ( x = +infty & y = +infty & z in REAL ) or ( x in REAL & y = -infty & z = -infty ) or ( x = -infty & y = -infty & z in REAL ) or ( x = -infty & y in REAL & z = -infty ) or ( x = -infty & y = -infty & z = -infty ) or ( x = +infty & y in REAL & z = +infty ) or ( x = +infty & y = +infty & z = +infty ) or ( x in REAL & y = +infty & z = +infty ) ) by A1, XXREAL_0:14;

suppose ( x in REAL & y in REAL & z in REAL ) ; :: thesis: (x + y) + z = x + (y + z)

then reconsider A = x, B = y, C = z as Real ;
( (A + B) + C = (x + y) + z & A + (B + C) = x + (y + z) ) ;
hence (x + y) + z = x + (y + z) ; :: thesis: verum

end;

suppose A2: ( x in REAL & y = +infty & z in REAL ) ; :: thesis: (x + y) + z = x + (y + z)

then ( x + y = +infty & y + z = +infty ) by Def2;
hence (x + y) + z = x + (y + z) by A2; :: thesis: verum

end;

suppose A3: ( x in REAL & y = -infty & z in REAL ) ; :: thesis: (x + y) + z = x + (y + z)

then ( x + y = -infty & y + z = -infty ) by Def2;
hence (x + y) + z = x + (y + z) by A3; :: thesis: verum

end;

suppose A4: ( x = -infty & y in REAL & z in REAL ) ; :: thesis: (x + y) + z = x + (y + z)

then x + y = -infty by Def2;
then (x + y) + z = -infty by A4, Def2;
hence (x + y) + z = x + (y + z) by A4, Def2; :: thesis: verum

end;

suppose A5: ( x = +infty & y in REAL & z in REAL ) ; :: thesis: (x + y) + z = x + (y + z)

then x + y = +infty by Def2;
then (x + y) + z = +infty by A5, Def2;
hence (x + y) + z = x + (y + z) by A5, Def2; :: thesis: verum

end;

suppose A6: ( x in REAL & y in REAL & z = +infty ) ; :: thesis: (x + y) + z = x + (y + z)

then y + z = +infty by Def2;
then x + (y + z) = +infty by A6, Def2;
hence (x + y) + z = x + (y + z) by A6, Def2; :: thesis: verum

end;

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

then y + z = -infty by Def2;
then x + (y + z) = -infty by A7, Def2;
hence (x + y) + z = x + (y + z) by A7, Def2; :: thesis: verum

end;

suppose A8: ( x = +infty & y = +infty & z in REAL ) ; :: thesis: (x + y) + z = x + (y + z)

then x + y = +infty by Def2;
then A9: (x + y) + z = +infty by A8, Def2;
y + z <> -infty by A8, Def2;
hence (x + y) + z = x + (y + z) by A8, A9, Def2; :: thesis: verum

end;

suppose A10: ( x in REAL & y = -infty & z = -infty ) ; :: thesis: (x + y) + z = x + (y + z)

then A11: x + y = -infty by Def2;
then (x + y) + z = -infty by A10, Def2;
hence (x + y) + z = x + (y + z) by A10, A11; :: thesis: verum

end;

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

then A13: x + y = -infty by Def2;
then (x + y) + z = -infty by A12, Def2;
hence (x + y) + z = x + (y + z) by A12, A13; :: thesis: verum

end;

suppose ( ( x = -infty & y in REAL & z = -infty ) or ( x = -infty & y = -infty & z = -infty ) or ( x = +infty & y in REAL & z = +infty ) or ( x = +infty & y = +infty & z = +infty ) ) ; :: thesis: (x + y) + z = x + (y + z)

hence (x + y) + z = x + (y + z) ; :: thesis: verum

end;

suppose A14: ( x in REAL & y = +infty & z = +infty ) ; :: thesis: (x + y) + z = x + (y + z)

then ( x + y = +infty & y + z = +infty ) by Def2;
hence (x + y) + z = x + (y + z) by A14; :: thesis: verum

end;

end;