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 by TOPS_2:64;
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 )
( the topology of T c= UniCl P & Int A in the topology of T ) by CANTOR_1:def 2, PRE_TOPC:def 2;
then consider Y being Subset-Family of T such that
A3: Y c= P and
A4: Int A = union Y by CANTOR_1:def 1;
reconsider Y = Y as Subset-Family of T ;
consider K being set such that
A5: p in K and
A6: K in Y by A2, A4, TARSKI:def 4;
reconsider K = K as Subset of T by A6;
take K ; :: thesis: ( K in P & p in Int K & K c= A )
thus K in P by A3, A6; :: thesis: ( p in Int K & K c= A )
then K is open by A1;
hence p in Int K by A5, TOPS_1:23; :: thesis: K c= A
A7: Int A c= A by TOPS_1:16;
K c= union Y by A6, ZFMISC_1:74;
hence K c= A by A4, A7; :: thesis: verum