let S, T be TopSpace; :: thesis: ( ex K being prebasis of S ex L being prebasis of T st
( [#] S in K & K = INTERSECTION (L,{([#] S)}) ) implies S is SubSpace of T )
given K being prebasis of S, L being prebasis of T such that A1: ( [#] S in K & K = INTERSECTION (L,{([#] S)}) ) ; :: thesis: S is SubSpace of T
consider B, S0 being set such that
A2: ( B in L & S0 in {([#] S)} & [#] S = B /\ S0 ) by A1, SETFAM_1:def 5;
B c= the carrier of T by A2;
then A3: B c= [#] T by STRUCT_0:def 3;
[#] S c= B by A2, XBOOLE_1:17;
hence S is SubSpace of T by A1, A3, Th50, XBOOLE_1:1; :: thesis: verum