let a, b be Real; :: thesis: for I being Subset of R^1 st I = [.a,b.] holds
I is compact
let I be Subset of R^1; :: thesis: ( I = [.a,b.] implies I is compact )
assume A1: I = [.a,b.] ; :: thesis: I is compact
per cases ( a <= b or a > b ) ;
suppose A2: a <= b ; :: thesis: I is compact
then Closed-Interval-TSpace (a,b) is compact by HEINE:4;
then A3: [#] (Closed-Interval-TSpace (a,b)) is compact by COMPTS_1:1;
[#] (Closed-Interval-TSpace (a,b)) = the carrier of (Closed-Interval-TSpace (a,b)) by STRUCT_0:def 3;
then I = [#] (Closed-Interval-TSpace (a,b)) by A1, A2, TOPMETR:18;
hence I is compact by A3, COMPTS_1:19; :: thesis: verum
end;
suppose a > b ; :: thesis: I is compact
then [.a,b.] = {} by XXREAL_1:29;
hence I is compact by A1; :: thesis: verum
end;
end;