let x, y, z be ExtReal; :: thesis:
assume not x is real ; :: thesis:
then A1: not x in REAL ;
assume A2: not x * (y * z) = (x * y) * z ; :: thesis:
then A3: ( y <> 0 & z <> 0 ) by Lm19, Lm20;

per cases by A1, XXREAL_0:14;

suppose A4: x = -infty ; :: thesis:

per cases by A3;

suppose A5: ( y is positive & z is positive ) ; :: thesis:

then -infty * (y * z) = -infty by Def5
.= -infty * z by A5, Def5
.= (-infty * y) * z by A5, Def5 ;
hence contradiction by A2, A4; :: thesis:

end;

suppose A6: ( y is positive & z is negative ) ; :: thesis:

then -infty * (y * z) = +infty by Def5
.= -infty * z by A6, Def5
.= (-infty * y) * z by A6, Def5 ;
hence contradiction by A2, A4; :: thesis:

end;

suppose A7: ( y is negative & z is positive ) ; :: thesis:

then -infty * (y * z) = +infty by Def5
.= +infty * z by A7, Def5
.= (-infty * y) * z by A7, Def5 ;
hence contradiction by A2, A4; :: thesis:

end;

suppose A8: ( y is negative & z is negative ) ; :: thesis:

then -infty * (y * z) = -infty by Def5
.= +infty * z by A8, Def5
.= (-infty * y) * z by A8, Def5 ;
hence contradiction by A2, A4; :: thesis:

end;

end;

end;

suppose A9: x = +infty ; :: thesis:

per cases by A3;

suppose A10: ( y is positive & z is positive ) ; :: thesis:

then +infty * (y * z) = +infty by Def5
.= +infty * z by A10, Def5
.= (+infty * y) * z by A10, Def5 ;
hence contradiction by A2, A9; :: thesis:

end;

suppose A11: ( y is positive & z is negative ) ; :: thesis:

then +infty * (y * z) = -infty by Def5
.= +infty * z by A11, Def5
.= (+infty * y) * z by A11, Def5 ;
hence contradiction by A2, A9; :: thesis:

end;

suppose A12: ( y is negative & z is positive ) ; :: thesis:

then +infty * (y * z) = -infty by Def5
.= -infty * z by A12, Def5
.= (+infty * y) * z by A12, Def5 ;
hence contradiction by A2, A9; :: thesis:

end;

suppose A13: ( y is negative & z is negative ) ; :: thesis:

then +infty * (y * z) = +infty by Def5
.= -infty * z by A13, Def5
.= (+infty * y) * z by A13, Def5 ;
hence contradiction by A2, A9; :: thesis:

end;

end;

end;

end;