let a, b be Real; for X being Subset of R^1 st X = ].a,b.] holds
Int X = ].a,b.[
let X be Subset of R^1; ( X = ].a,b.] implies Int X = ].a,b.[ )
assume A1:
X = ].a,b.]
; Int X = ].a,b.[
A2:
Int X c= X
by TOPS_1:16;
thus
Int X c= ].a,b.[
XBOOLE_0:def 10 ].a,b.[ c= Int Xproof
let x be
object ;
TARSKI:def 3 ( not x in Int X or x in ].a,b.[ )
assume A3:
x in Int X
;
x in ].a,b.[
then reconsider x =
x as
Point of
R^1 ;
x <= b
by A1, A2, A3, XXREAL_1:2;
then A6:
x < b
by A4, XXREAL_0:1;
a < x
by A1, A2, A3, XXREAL_1:2;
hence
x in ].a,b.[
by A6, XXREAL_1:4;
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:41;
hence
].a,b.[ c= Int X
; verum