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

( [#] 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