theorem :: FINTOPO8:56

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