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) ) )

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

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

the carrier of S in the topology of S
by PRE_TOPC:def 1;
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) ) )

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

for x being Subset of S st x in X holds

x is open

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;( 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 )

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 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

( 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

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) )

end;( 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

then reconsider Y = { D where D is Subset of T : ( D in L & ex C being Element of K st
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;( 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

( 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

then
Y is open
by TOPS_2:def 1;
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;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

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

hence
A = B /\ ([#] S)
by TARSKI:2; :: thesis: verum
let x be object ; :: thesis: ( x in A iff x in B /\ ([#] S) )

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;hereby :: thesis: ( x in B /\ ([#] S) implies x in A )

assume A10:
x in B /\ ([#] S)
; :: thesis: x in Aassume
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;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

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

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

then reconsider X = INTERSECTION (Y,{([#] S)}) as Subset-Family of S ;
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;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

for x being Subset of S st x in X holds

x is open

proof

then A19:
X is open
by TOPS_2:def 1;
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;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

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

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