let S, T be TopSpace; :: thesis: ( ex K being Basis of S ex L being Basis of T st K = INTERSECTION (L,{([#] S)}) implies S is SubSpace of T )
given K being Basis of S, L being Basis of T such that A1: K = INTERSECTION (L,{([#] S)}) ; :: thesis: S is SubSpace of T
A2: for A being Subset of S holds
( A in the topology of S iff ex B being Subset of T st
( B in the topology of T & A = B /\ ([#] S) ) )

proof

let A be Subset of S; :: thesis: ( A in the topology of S iff ex B being Subset of T st
( B in the topology of T & A = B /\ ([#] S) ) )

hereby :: thesis: ( ex B being Subset of T st
( B in the topology of T & A = B /\ ([#] S) ) implies A in the topology of S )

assume A in the topology of S ; :: thesis: ex B being Element of bool the carrier of T st
( B in the topology of T & A = B /\ ([#] S) )
then A in UniCl K by CANTOR_1:def 2, TARSKI:def 3;
then consider X being Subset-Family of S such that
A3: ( X c= K & A = union X ) by CANTOR_1:def 1;
set Y = { D where D is Subset of T : ( D in L & ex C being Element of K st
( C in X & C = D /\ ([#] S) ) ) } ;
{ D where D is Subset of T : ( D in L & ex C being Element of K st
( C in X & C = D /\ ([#] S) ) ) } c= bool the carrier of T

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { D where D is Subset of T : ( D in L & ex C being Element of K st
( C in X & C = D /\ ([#] S) ) ) } or x in bool the carrier of T )
assume x in { D where D is Subset of T : ( D in L & ex C being Element of K st
( C in X & C = D /\ ([#] S) ) ) } ; :: thesis: x in bool the carrier of T
then ex D being Subset of T st
( D = x & D in L & ex C being Element of K st
( C in X & C = D /\ ([#] S) ) ) ;
hence x in bool the carrier of T ; :: thesis: verum

end;

then reconsider Y = { D where D is Subset of T : ( D in L & ex C being Element of K st
( C in X & C = D /\ ([#] S) ) ) } as Subset-Family of T ;
set B = union Y;
take B = union Y; :: thesis: ( B in the topology of T & A = B /\ ([#] S) )
for x being Subset of T st x in Y holds
x is open

proof

let x be Subset of T; :: thesis: ( x in Y implies x is open )
assume x in Y ; :: thesis: x is open
then ex D being Subset of T st
( D = x & D in L & ex C being Element of K st
( C in X & C = D /\ ([#] S) ) ) ;
hence x is open by TOPS_2:def 1; :: thesis: verum

end;

then Y is open by TOPS_2:def 1;
hence B in the topology of T by TOPS_2:19, PRE_TOPC:def 2; :: thesis: A = B /\ ([#] S)
for x being object holds
( x in A iff x in B /\ ([#] S) )

proof

let x be object ; :: thesis: ( x in A iff x in B /\ ([#] S) )

hereby :: thesis: ( x in B /\ ([#] S) implies x in A )

assume x in A ; :: thesis: x in B /\ ([#] S)
then consider C being set such that
A6: ( x in C & C in X ) by A3, TARSKI:def 4;
reconsider C = C as Element of K by A3, A6;
consider D, S0 being set such that
A7: ( D in L & S0 in {([#] S)} & C = D /\ S0 ) by A1, A3, A6, SETFAM_1:def 5;
reconsider D = D as Subset of T by A7;
( C in X & C = D /\ ([#] S) ) by A6, A7, TARSKI:def 1;
then A8: D in Y by A7;
x in D by A6, A7, XBOOLE_0:def 4;
then A9: x in B by A8, TARSKI:def 4;
x in S0 by A6, A7, XBOOLE_0:def 4;
then x in [#] S by A7, TARSKI:def 1;
hence x in B /\ ([#] S) by A9, XBOOLE_0:def 4; :: thesis: verum

end;

assume A10: x in B /\ ([#] S) ; :: thesis: x in A
then x in B by XBOOLE_0:def 4;
then consider D0 being set such that
A11: ( x in D0 & D0 in Y ) by TARSKI:def 4;
consider D being Subset of T such that
A12: ( D = D0 & D in L ) and
A13: ex C being Element of K st
( C in X & C = D /\ ([#] S) ) by A11;
consider C being Element of K such that
A14: ( C in X & C = D /\ ([#] S) ) by A13;
x in [#] S by A10, XBOOLE_0:def 4;
then x in C by A11, A12, A14, XBOOLE_0:def 4;
hence x in A by A3, A14, TARSKI:def 4; :: thesis: verum

end;

hence A = B /\ ([#] S) by TARSKI:2; :: thesis: verum

end;

given B being Subset of T such that A15: ( B in the topology of T & A = B /\ ([#] S) ) ; :: thesis: A in the topology of S
B in UniCl L by A15, CANTOR_1:def 2, TARSKI:def 3;
then consider Y being Subset-Family of T such that
A16: ( Y c= L & B = union Y ) by CANTOR_1:def 1;
set X = INTERSECTION (Y,{([#] S)});
INTERSECTION (Y,{([#] S)}) c= bool the carrier of S

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in INTERSECTION (Y,{([#] S)}) or x in bool the carrier of S )
reconsider x0 = x as set by TARSKI:1;
assume x in INTERSECTION (Y,{([#] S)}) ; :: thesis: x in bool the carrier of S
then consider C, S0 being set such that
A17: ( C in Y & S0 in {([#] S)} & x0 = C /\ S0 ) by SETFAM_1:def 5;
x0 c= S0 by A17, XBOOLE_1:17;
then x0 c= [#] S by A17, TARSKI:def 1;
then x0 c= the carrier of S by STRUCT_0:def 3;
hence x in bool the carrier of S ; :: thesis: verum

end;

then reconsider X = INTERSECTION (Y,{([#] S)}) as Subset-Family of S ;
for x being Subset of S st x in X holds
x is open

proof

let x be Subset of S; :: thesis: ( x in X implies x is open )
assume x in X ; :: thesis: x is open
then consider C, S0 being set such that
A18: ( C in Y & S0 in {([#] S)} & x = C /\ S0 ) by SETFAM_1:def 5;
x in K by A1, A16, A18, SETFAM_1:def 5;
hence x is open by TOPS_2:def 1; :: thesis: verum

end;

then A19: X is open by TOPS_2:def 1;
A = union X by A15, A16, SETFAM_1:25;
hence A in the topology of S by A19, TOPS_2:19, PRE_TOPC:def 2; :: thesis: verum

end;

the carrier of S in the topology of S by PRE_TOPC:def 1;
then consider B being Subset of T such that
A20: ( B in the topology of T & the carrier of S = B /\ ([#] S) ) by A2;
[#] S = B /\ ([#] S) by A20, STRUCT_0:def 3;
then [#] S c= B by XBOOLE_1:17;
then [#] S c= the carrier of T by XBOOLE_1:1;
then [#] S c= [#] T by STRUCT_0:def 3;
hence S is SubSpace of T by A2, PRE_TOPC:def 4; :: thesis: verum