let A be Interval; :: thesis: 0 ** A is interval

per cases ( A = {} or A <> {} ) ;

suppose A = {} ; :: thesis: 0 ** A is interval

hence 0 ** A is interval ; :: thesis: verum

end;

suppose A <> {} ; :: thesis: 0 ** A is interval

then 0 ** A = {0} by Th3;
then 0 ** A = [.0,0.] by XXREAL_1:17;
hence 0 ** A is interval ; :: thesis: verum

end;

end;