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
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { ].a,b.[ where a, b is Real : a < b } or x in bool the carrier of FMT_R^1 )
assume x in { ].a,b.[ where a, b is Real : a < b } ; :: thesis: x in bool the carrier of FMT_R^1
then ex a, b being Real st
( x = ].a,b.[ & a < b ) ;
then reconsider x = x as Subset of REAL ;
x in bool the carrier of FMT_R^1 by A2;
hence x in bool the carrier of FMT_R^1 ; :: thesis: verum
end;
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
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in BA or x in Family_open_set FMT_R^1 )
assume A3: x in BA ; :: thesis: x in Family_open_set FMT_R^1
then reconsider x = x as Subset of FMT_R^1 ;
consider a, b being Real such that
A4: x = ].a,b.[ and
a < b by A3;
now :: thesis: for y being Real st y in x holds
ex r being Real st
( r > 0 & ].(y - r),(y + r).[ c= x )
let y be Real; :: thesis: ( y in x implies ex r being Real st
( r > 0 & ].(y - r),(y + r).[ c= x ) )
assume A5: y in x ; :: thesis: ex r being Real st
( r > 0 & ].(y - r),(y + r).[ c= x )
reconsider z = x as Subset of R^1 by FINTOPO7:def 15;
z is open by A4, JORDAN6:35;
hence ex r being Real st
( r > 0 & ].(y - r),(y + r).[ c= x ) by A5, FRECHET:8; :: thesis: verum
end;
then x is open by Th55;
then x in { O where O is open Subset of FMT_R^1 : verum } ;
hence x in Family_open_set FMT_R^1 by FINTOPO7:def 11; :: thesis: verum
end;
then reconsider BA = BA as open Subset-Family of FMT_R^1 by FINTOPO7:def 14;
now :: thesis: for x being object st x in Family_open_set FMT_R^1 holds
x in UniCl BA
let x be object ; :: thesis: ( x in Family_open_set FMT_R^1 implies x in UniCl BA )
assume x in Family_open_set FMT_R^1 ; :: thesis: x in UniCl BA
then x in { O where O is open Subset of FMT_R^1 : verum } by FINTOPO7:def 11;
then consider O being open Subset of FMT_R^1 such that
A6: x = O ;
NTop2Top FMT_R^1 = R^1 by FINTOPO7:24;
then O is open Subset of R^1 by Lm9;
then O in the topology of R^1 by PRE_TOPC:def 2;
then consider Y being Subset-Family of R^1 such that
A7: Y c= BBA and
A8: O = union Y by A1, CANTOR_1:def 1;
reconsider Y = Y as Subset-Family of FMT_R^1 by FINTOPO7:def 15;
Y c= BA by A7;
hence x in UniCl BA by A8, A6, CANTOR_1:def 1; :: thesis: verum
end;
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; :: thesis: verum