let T be TopSpace; :: thesis: for P being Basis of T holds P is basis of T
let P be Basis of T; :: thesis: P is basis of T
A1: ( P c= the topology of T & the topology of T c= UniCl P ) by CANTOR_1:def 2;
let p be Point of T; :: according to YELLOW13:def 4 :: thesis: P is basis of p
let A be Subset of T; :: according to YELLOW13:def 1 :: thesis: ( p in Int A implies ex P being Subset of T st
( P in P & p in Int P & P c= A ) )
assume A2: p in Int A ; :: thesis: ex P being Subset of T st
( P in P & p in Int P & P c= A )
Int A in the topology of T by PRE_TOPC:def 5;
then consider Y being Subset-Family of T such that
A3: ( Y c= P & Int A = union Y ) by A1, CANTOR_1:def 1;
reconsider Y = Y as Subset-Family of T ;
consider K being set such that
A4: ( p in K & K in Y ) by A2, A3, TARSKI:def 4;
reconsider K = K as Subset of T by A4;
take K ; :: thesis: ( K in P & p in Int K & K c= A )
thus K in P by A3, A4; :: thesis: ( p in Int K & K c= A )
then K is open by A1, PRE_TOPC:def 5;
hence p in Int K by A4, TOPS_1:55; :: thesis: K c= A
A5: K c= union Y by A4, ZFMISC_1:92;
Int A c= A by TOPS_1:44;
hence K c= A by A3, A5, XBOOLE_1:1; :: thesis: verum