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

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

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

hence 0 ** A is connected by Th5; :: thesis: verum

end;

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

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

end;

end;