let a, b be real number ; :: thesis: for X being Subset of R^1 st X = [.a,b.] holds
Int X = ].a,b.[
let X be Subset of R^1 ; :: thesis: ( X = [.a,b.] implies Int X = ].a,b.[ )
assume A1: X = [.a,b.] ; :: thesis: Int X = ].a,b.[
reconsider Y = ].a,b.[ as open Subset of R^1 by BORSUK_5:62, TOPMETR:24;
A2: Int X c= X by TOPS_1:44;
thus Int X c= ].a,b.[ :: according to XBOOLE_0:def 10 :: thesis: ].a,b.[ c= Int X

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Int X or x in ].a,b.[ )
assume A3: x in Int X ; :: thesis: x in ].a,b.[
then reconsider x = x as Point of R^1 ;

A4: now

assume A5: ( x = a or x = b ) ; :: thesis: contradiction
A6: Int X misses Fr X by TOPS_1:73;

now

assume a > b ; :: thesis: contradiction
then X = {} R^1 by A1, XXREAL_1:29;
hence contradiction by A3; :: thesis: verum

end;

then Fr X = {a,b} by A1, Th44;
then ( a in Fr X & b in Fr X ) by TARSKI:def 2;
hence contradiction by A3, A5, A6, XBOOLE_0:3; :: thesis: verum

end;

( a <= x & x <= b ) by A1, A2, A3, XXREAL_1:1;
then ( a < x & x < b ) by A4, XXREAL_0:1;
hence x in ].a,b.[ by XXREAL_1:4; :: thesis: verum

end;

Y c= Int X by A1, TOPS_1:56, XXREAL_1:37;
hence ].a,b.[ c= Int X ; :: thesis: verum