let X be Subset of REAL; :: thesis: ( X = ].a,b.[ iff for x being R_eal holds

( x in X iff ( a < x & x < b ) ) )

thus ( X = ].a,b.[ implies for x being R_eal holds

( x in X iff ( a < x & x < b ) ) ) by XXREAL_1:4; :: thesis: ( ( for x being R_eal holds

( x in X iff ( a < x & x < b ) ) ) implies X = ].a,b.[ )

assume A1: for x being R_eal holds

( x in X iff ( a < x & x < b ) ) ; :: thesis: X = ].a,b.[

thus X c= ].a,b.[ :: according to XBOOLE_0:def 10 :: thesis: ].a,b.[ c= X

reconsider t = x as R_eal by XXREAL_0:def 1;

assume x in ].a,b.[ ; :: thesis: x in X

then ( a < t & t < b ) by XXREAL_1:4;

hence x in X by A1; :: thesis: verum

( x in X iff ( a < x & x < b ) ) )

thus ( X = ].a,b.[ implies for x being R_eal holds

( x in X iff ( a < x & x < b ) ) ) by XXREAL_1:4; :: thesis: ( ( for x being R_eal holds

( x in X iff ( a < x & x < b ) ) ) implies X = ].a,b.[ )

assume A1: for x being R_eal holds

( x in X iff ( a < x & x < b ) ) ; :: thesis: X = ].a,b.[

thus X c= ].a,b.[ :: according to XBOOLE_0:def 10 :: thesis: ].a,b.[ c= X

proof

let x be Real; :: according to MEMBERED:def 9 :: thesis: ( not x in ].a,b.[ or x in X )
let x be Real; :: according to MEMBERED:def 9 :: thesis: ( not x in X or x in ].a,b.[ )

assume A2: x in X ; :: thesis: x in ].a,b.[

then x in REAL ;

then reconsider t = x as R_eal by NUMBERS:31;

( a < t & t < b ) by A1, A2;

hence x in ].a,b.[ ; :: thesis: verum

end;assume A2: x in X ; :: thesis: x in ].a,b.[

then x in REAL ;

then reconsider t = x as R_eal by NUMBERS:31;

( a < t & t < b ) by A1, A2;

hence x in ].a,b.[ ; :: thesis: verum

reconsider t = x as R_eal by XXREAL_0:def 1;

assume x in ].a,b.[ ; :: thesis: x in X

then ( a < t & t < b ) by XXREAL_1:4;

hence x in X by A1; :: thesis: verum