let A1, A2 be non empty strict compact TopSpace; :: thesis: ( ex a, b being Real st
( a <= b & [.a,b.] = A & A1 = Closed-Interval-TSpace (a,b) ) & ex a, b being Real st
( a <= b & [.a,b.] = A & A2 = Closed-Interval-TSpace (a,b) ) implies A1 = A2 )
assume that
A4: ex a, b being Real st
( a <= b & [.a,b.] = A & A1 = Closed-Interval-TSpace (a,b) ) and
A5: ex a, b being Real st
( a <= b & [.a,b.] = A & A2 = Closed-Interval-TSpace (a,b) ) ; :: thesis: A1 = A2
consider a1, b1 being Real such that
A6: ( a1 <= b1 & [.a1,b1.] = A & A1 = Closed-Interval-TSpace (a1,b1) ) by A4;
consider a2, b2 being Real such that
A7: ( a2 <= b2 & [.a2,b2.] = A & A2 = Closed-Interval-TSpace (a2,b2) ) by A5;
( a1 = a2 & b1 = b2 ) by A6, A7, XXREAL_1:66;
hence A1 = A2 by A6, A7; :: thesis: verum