let a, b be Real; :: 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.[
A2: Int X c= X by TOPS_1:16;
thus Int X c= ].a,b.[ :: according to XBOOLE_0:def 10 :: thesis: ].a,b.[ c= Int X
proof
let x be object ; :: 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 :: thesis: not x = a
then Fr X = {a,b} by A1, Th34;
then A5: ( Int X misses Fr X & a in Fr X ) by TARSKI:def 2, TOPS_1:39;
assume x = a ; :: thesis: contradiction
hence contradiction by A3, A5, XBOOLE_0:3; :: thesis: verum
end;
a <= x by A1, A2, A3, XXREAL_1:3;
then A6: a < x by A4, XXREAL_0:1;
x < b by A1, A2, A3, XXREAL_1:3;
hence x in ].a,b.[ by A6, XXREAL_1:4; :: thesis: verum
end;
reconsider Y = ].a,b.[ as open Subset of R^1 by BORSUK_5:39, TOPMETR:17;
Y c= Int X by A1, TOPS_1:24, XXREAL_1:45;
hence ].a,b.[ c= Int X ; :: thesis: verum