let T be TopSpace; :: thesis: for A being Subset of T
for Bas being Basis of T holds Bas | A is Basis of T | A
let A be Subset of T; :: thesis: for Bas being Basis of T holds Bas | A is Basis of T | A
let Bas be Basis of T; :: thesis: Bas | A is Basis of T | A
set BasA = Bas | A;
set TA = T | A;
A1: for U being Subset of (T | A) st U is open holds
for p being Point of (T | A) st p in U holds
ex a being Subset of (T | A) st
( a in Bas | A & p in a & a c= U )

proof

let U be Subset of (T | A); :: thesis: ( U is open implies for p being Point of (T | A) st p in U holds
ex a being Subset of (T | A) st
( a in Bas | A & p in a & a c= U ) )
assume A2: U is open ; :: thesis: for p being Point of (T | A) st p in U holds
ex a being Subset of (T | A) st
( a in Bas | A & p in a & a c= U )
consider W being Subset of T such that
A3: W is open and
A4: U = W /\ the carrier of (T | A) by A2, TSP_1:def 1;
let p be Point of (T | A); :: thesis: ( p in U implies ex a being Subset of (T | A) st
( a in Bas | A & p in a & a c= U ) )
assume A5: p in U ; :: thesis: ex a being Subset of (T | A) st
( a in Bas | A & p in a & a c= U )
p in W by A4, A5, XBOOLE_0:def 4;
then consider Wb being Subset of T such that
A6: Wb in Bas and
A7: p in Wb and
A8: Wb c= W by A3, YELLOW_9:31;
A9: Wb /\ A in Bas | A by A6, TOPS_2:41;
then reconsider WbA = Wb /\ A as Subset of (T | A) ;
A10: [#] (T | A) = A by PRE_TOPC:def 10;
then p in WbA by A5, A7, XBOOLE_0:def 4;
hence ex a being Subset of (T | A) st
( a in Bas | A & p in a & a c= U ) by A4, A8, A9, A10, XBOOLE_1:26; :: thesis: verum

end;

Bas | A c= the topology of (T | A)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Bas | A or x in the topology of (T | A) )
assume A11: x in Bas | A ; :: thesis: x in the topology of (T | A)
reconsider U = x as Subset of (T | A) by A11;
Bas c= the topology of T by CANTOR_1:def 2;
then Bas is open by CANTOR_1:3, TOPS_2:18;
then Bas | A is open by TOPS_2:47;
then U is open by A11, TOPS_2:def 1;
hence x in the topology of (T | A) by PRE_TOPC:def 5; :: thesis: verum

end;

hence Bas | A is Basis of T | A by A1, YELLOW_9:32; :: thesis: verum