set BA = { ].a,b.[ where a, b is Real : a < b } ;
reconsider BBA = { ].a,b.[ where a, b is Real : a < b } as open quasi_basis Subset-Family of R^1 by TOPGEN_5:72;
A1:
the topology of R^1 c= UniCl BBA
by CANTOR_1:def 2;
A2:
the carrier of FMT_R^1 = REAL
by TOPMETR:17, FINTOPO7:def 15;
{ ].a,b.[ where a, b is Real : a < b } c= bool the carrier of FMT_R^1
then reconsider BA = { ].a,b.[ where a, b is Real : a < b } as Subset-Family of FMT_R^1 ;
BA c= Family_open_set FMT_R^1
then reconsider BA = BA as open Subset-Family of FMT_R^1 by FINTOPO7:def 14;
then
Family_open_set FMT_R^1 c= UniCl BA
;
hence
{ ].a,b.[ where a, b is Real : a < b } is Basis of FMT_R^1
by FINTOPO7:def 13; verum