let A be non empty 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 Th6; :: thesis: verum

end;

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

now :: thesis: ( ( A is open_interval & x ** A is Interval ) or ( A is closed_interval & x ** A is Interval ) or ( A is right_open_interval & ( ( x < 0 & x ** A is Interval ) or ( 0 < x & x ** A is Interval ) ) ) or ( A is left_open_interval & x ** A is Interval ) )

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:1;

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

then x ** A is open_interval by A1, Th7;
hence x ** A is Interval ; :: thesis: verum

end;

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

then x ** A is closed_interval by A1, Th8;
hence x ** A is Interval ; :: 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, Th10;
hence x ** A is Interval ; :: thesis: verum

end;

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

then x ** A is right_open_interval by A2, Th9;
hence x ** A is Interval ; :: thesis: verum

end;

end;

end;

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

now :: thesis: ( ( x < 0 & x ** A is Interval ) or ( 0 < x & x ** A is Interval ) )

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, Th12;
hence x ** A is Interval ; :: thesis: verum

end;

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

then x ** A is left_open_interval by A3, Th11;
hence x ** A is Interval ; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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

end;

end;