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
proof
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;
let x be Real; :: according to MEMBERED:def 9 :: thesis: ( not x in ].a,b.[ or x in 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