for x being set st x in ].a,b.[ holds
x in REAL ;
hence ].a,b.[ is Subset of REAL ; :: thesis: verum