let r be set ; :: thesis: for I being interval Subset of REAL st r in I & I is open_interval holds
r in ].(inf I),(sup I).[
let I be interval Subset of REAL; :: thesis: ( r in I & I is open_interval implies r in ].(inf I),(sup I).[ )
assume that
A1: r in I and
A2: I is open_interval ; :: thesis: r in ].(inf I),(sup I).[
consider a, b being R_eal such that
A3: I = ].a,b.[ by A2, MEASURE5:def 2;
reconsider r1 = r as Real by A1;
A4: ( a < r1 & r1 < b ) by A1, A3, XXREAL_1:4;
a < b by A4, XXREAL_0:2;
then ( inf I = a & sup I = b ) by A3, XXREAL_2:28, XXREAL_2:32;
hence r in ].(inf I),(sup I).[ by A1, A3; :: thesis: verum