theorem Th3: :: FUZZY_9:5

for a, b being Real holds
( a in REAL \ ].a,b.[ & b in REAL \ ].a,b.[ )