theorem Th57: :: FINTOPO8:57

{ ].a,b.[ where a, b is Real : a < b } is Basis of FMT_R^1