:: deftheorem defines ]. MEASURE5:def 1 :
for a, b being R_eal
for b₃ being Subset of REAL holds
( b₃ = ].a,b.[ iff for x being R_eal holds
( x in b₃ iff ( a < x & x < b ) ) );