let I be Interval; :: thesis: for x being Real st x in I & x <> inf I & x <> sup I holds
x in ].(inf I),(sup I).[
let x be Real; :: thesis: ( x in I & x <> inf I & x <> sup I implies x in ].(inf I),(sup I).[ )
assume that
A1: x in I and
A2: x <> inf I and
A3: x <> sup I ; :: thesis: x in ].(inf I),(sup I).[
( inf I <= x & x <= sup I ) by A1, XXREAL_2:61, XXREAL_2:62;
then ( inf I < x & x < sup I ) by A2, A3, XXREAL_0:1;
hence x in ].(inf I),(sup I).[ by XXREAL_1:4; :: thesis: verum