let T be TopSpace; 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; for Bas being Basis of T holds Bas | A is Basis of (T | A)
let Bas be Basis of T; 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);
( 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
;
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);
( 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
;
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;
verum
end;
Bas | A c= the topology of (T | A)
hence
Bas | A is Basis of (T | A)
by A1, YELLOW_9:32; verum