let T be non empty TopSpace; :: thesis: for S being SubSpace of T
for B being Basis of T holds { (A /\ ([#] S)) where A is Subset of T : ( A in B & A meets [#] S ) } is Basis of S
let S be SubSpace of T; :: thesis: for B being Basis of T holds { (A /\ ([#] S)) where A is Subset of T : ( A in B & A meets [#] S ) } is Basis of S
let B be Basis of T; :: thesis: { (A /\ ([#] S)) where A is Subset of T : ( A in B & A meets [#] S ) } is Basis of S
set X = { (A /\ ([#] S)) where A is Subset of T : ( A in B & A meets [#] S ) } ;
{ (A /\ ([#] S)) where A is Subset of T : ( A in B & A meets [#] S ) } c= bool the carrier of S

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in { (A /\ ([#] S)) where A is Subset of T : ( A in B & A meets [#] S ) } or u in bool the carrier of S )
assume u in { (A /\ ([#] S)) where A is Subset of T : ( A in B & A meets [#] S ) } ; :: thesis: u in bool the carrier of S
then ex A being Subset of T st
( u = A /\ ([#] S) & A in B & A meets [#] S ) ;
hence u in bool the carrier of S ; :: thesis: verum

end;

then reconsider X = { (A /\ ([#] S)) where A is Subset of T : ( A in B & A meets [#] S ) } as Subset-Family of S ;

A1: now :: thesis: for U being Subset of S st U is open holds
for x being Point of S st x in U holds
ex V being Subset of S st
( V in X & x in V & V c= U )

let U be Subset of S; :: thesis: ( U is open implies for x being Point of S st x in U holds
ex V being Subset of S st
( V in X & x in V & V c= U ) )
assume U is open ; :: thesis: for x being Point of S st x in U holds
ex V being Subset of S st
( V in X & x in V & V c= U )
then consider U0 being Subset of T such that
A2: U0 is open and
A3: U = U0 /\ the carrier of S by TSP_1:def 1;
let x be Point of S; :: thesis: ( x in U implies ex V being Subset of S st
( V in X & x in V & V c= U ) )
assume A4: x in U ; :: thesis: ex V being Subset of S st
( V in X & x in V & V c= U )
then x in U0 by A3, XBOOLE_0:def 4;
then consider V0 being Subset of T such that
A5: V0 in B and
A6: x in V0 and
A7: V0 c= U0 by A2, YELLOW_9:31;
reconsider V = V0 /\ ([#] S) as Subset of S ;
take V = V; :: thesis: ( V in X & x in V & V c= U )
V0 meets [#] S by A4, A6, XBOOLE_0:3;
hence V in X by A5; :: thesis: ( x in V & V c= U )
thus x in V by A4, A6, XBOOLE_0:def 4; :: thesis: V c= U
thus V c= U by A3, A7, XBOOLE_1:26; :: thesis: verum

end;

X c= the topology of S

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in X or u in the topology of S )
assume u in X ; :: thesis: u in the topology of S
then A8: ex A being Subset of T st
( u = A /\ ([#] S) & A in B & A meets [#] S ) ;
B c= the topology of T by TOPS_2:64;
hence u in the topology of S by A8, PRE_TOPC:def 4; :: thesis: verum

end;

hence { (A /\ ([#] S)) where A is Subset of T : ( A in B & A meets [#] S ) } is Basis of S by A1, YELLOW_9:32; :: thesis: verum