consider a, b being Real such that
A1: [.a,b.] = A by MEASURE5:def 3;
consider p being object such that
A2: p in A by XBOOLE_0:def 1;
consider r being Real such that
A3: ( r = p & a <= r & r <= b ) by A1, A2;
Closed-Interval-TSpace (a,b) is compact by A3, HEINE:4, XXREAL_0:2;
hence ex b₁ being non empty strict compact TopSpace ex a, b being Real st
( a <= b & [.a,b.] = A & b₁ = Closed-Interval-TSpace (a,b) ) by A1, A3, XXREAL_0:2; :: thesis: verum