let A be Interval; :: thesis: for x being Real holds x ** A is Interval
let x be Real; :: thesis: x ** A is Interval

per cases ( x = 0 or x <> 0 ) ;

suppose x = 0 ; :: thesis: x ** A is Interval

hence x ** A is Interval by Th8; :: thesis: verum

end;

suppose A1: x <> 0 ; :: thesis: x ** A is Interval

now

per cases ( A is open_interval or A is closed_interval or A is right_open_interval or A is left_open_interval ) by MEASURE5:def 9;

case A is open_interval ; :: thesis: x ** A is Interval

then x ** A is open_interval by A1, Th9;
hence x ** A is Interval by MEASURE5:def 9; :: thesis: verum

end;

case A is closed_interval ; :: thesis: x ** A is Interval

then x ** A is closed_interval by A1, Th10;
hence x ** A is Interval by MEASURE5:def 9; :: thesis: verum

end;

case A2: A is right_open_interval ; :: thesis: verum

per cases ( x < 0 or 0 < x ) by A1;

case x < 0 ; :: thesis: x ** A is Interval

then x ** A is left_open_interval by A2, Th12;
hence x ** A is Interval by MEASURE5:def 9; :: thesis: verum

end;

case 0 < x ; :: thesis: x ** A is Interval

then x ** A is right_open_interval by A2, Th11;
hence x ** A is Interval by MEASURE5:def 9; :: thesis: verum

end;

end;

end;

case A3: A is left_open_interval ; :: thesis: x ** A is Interval

now

per cases ( x < 0 or 0 < x ) by A1;

case x < 0 ; :: thesis: x ** A is Interval

then x ** A is right_open_interval by A3, Th14;
hence x ** A is Interval by MEASURE5:def 9; :: thesis: verum

end;

case 0 < x ; :: thesis: x ** A is Interval

then x ** A is left_open_interval by A3, Th13;
hence x ** A is Interval by MEASURE5:def 9; :: thesis: verum

end;

end;

end;

hence x ** A is Interval ; :: thesis: verum

end;

end;

end;

hence x ** A is Interval ; :: thesis: verum

end;

end;