theorem Th51: :: TOPS_5:51
for S, T being TopSpace st ex K being prebasis of S ex L being prebasis of T st
( [#] S in K & K = INTERSECTION (L,{([#] S)}) ) holds
S is SubSpace of T