theorem Th72: :: TOPGEN_5:72

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