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 ( A is open_interval or A is closed_interval or A is right_open_interval or A is left_open_interval ) by MEASURE5:1;

suppose A is open_interval ; :: thesis: x ++ A is Interval

then x ++ A is open_interval by Th26;
hence x ++ A is Interval ; :: thesis: verum

end;

suppose A is closed_interval ; :: thesis: x ++ A is Interval

then x ++ A is closed_interval by Th27;
hence x ++ A is Interval ; :: thesis: verum

end;

suppose A is right_open_interval ; :: thesis: x ++ A is Interval

then x ++ A is right_open_interval by Th28;
hence x ++ A is Interval ; :: thesis: verum

end;

suppose A is left_open_interval ; :: thesis: x ++ A is Interval

then x ++ A is left_open_interval by Th29;
hence x ++ A is Interval ; :: thesis: verum

end;

end;