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 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 )
then consider W being Subset of T such that
A2: W is open and
A3: U = W /\ the carrier of (T | A) by 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 A4: 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 A3, A4, XBOOLE_0:def 4;
then consider Wb being Subset of T such that
A5: Wb in Bas and
A6: p in Wb and
A7: Wb c= W by A2, YELLOW_9:31;
A8: Wb /\ A in Bas | A by A5, TOPS_2:31;
then reconsider WbA = Wb /\ A as Subset of (T | A) ;
A9: [#] (T | A) = A by PRE_TOPC:def 5;
then p in WbA by A4, A6, XBOOLE_0:def 4;
hence ex a being Subset of (T | A) st
( a in Bas | A & p in a & a c= U ) by A3, A7, A8, A9, XBOOLE_1:26; :: thesis: verum

end;

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Bas | A or x in the topology of (T | A) )
assume A10: x in Bas | A ; :: thesis: x in the topology of (T | A)
reconsider U = x as Subset of (T | A) by A10;
Bas | A is open by TOPS_2:37;
then U is open by A10;
hence x in the topology of (T | A) ; :: thesis: verum

end;

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