let X be non empty SubSpace of M; :: thesis: ( X is open implies ( X is without_boundary & X is n -manifold ) )

assume A1: X is open ; :: thesis: ( X is without_boundary & X is n -manifold )

[#] X c= [#] M by PRE_TOPC:def 4;

then reconsider X1 = [#] X as non empty open Subset of M by A1, TSEP_1:def 1;

A2: the carrier of X = [#] (M | X1) by PRE_TOPC:def 5

.= the carrier of (M | X1) ;

then A3: TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of (M | X1), the topology of (M | X1) #) by TSEP_1:5;

for p being Point of X ex U being a_neighborhood of p ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic

assume A1: X is open ; :: thesis: ( X is without_boundary & X is n -manifold )

[#] X c= [#] M by PRE_TOPC:def 4;

then reconsider X1 = [#] X as non empty open Subset of M by A1, TSEP_1:def 1;

A2: the carrier of X = [#] (M | X1) by PRE_TOPC:def 5

.= the carrier of (M | X1) ;

then A3: TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of (M | X1), the topology of (M | X1) #) by TSEP_1:5;

for p being Point of X ex U being a_neighborhood of p ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic

proof

hence
( X is without_boundary & X is n -manifold )
by Def4; :: thesis: verum
let p be Point of X; :: thesis: ex U being a_neighborhood of p ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic

p in the carrier of X ;

then reconsider p1 = p as Point of M by A2;

consider U1 being a_neighborhood of p1, S1 being open Subset of (TOP-REAL n) such that

A8: U1,S1 are_homeomorphic by Def4;

consider U2 being open Subset of M, S2 being open Subset of (TOP-REAL n) such that

A9: ( U2 c= U1 & p1 in U2 & U2,S2 are_homeomorphic ) by A8, Th11;

reconsider X2 = X as non empty open SubSpace of M by A1;

reconsider U = U2 /\ X1 as Subset of X2 by XBOOLE_1:17;

A10: M | U2,(TOP-REAL n) | S2 are_homeomorphic by A9, METRIZTS:def 1;

consider f being Function of (M | U2),((TOP-REAL n) | S2) such that

A11: f is being_homeomorphism by T_0TOPSP:def 1, A9, METRIZTS:def 1;

A12: p in U2 /\ X1 by A9, XBOOLE_0:def 4;

U is open by TSEP_1:17;

then reconsider U = U as a_neighborhood of p by A12, CONNSP_2:3;

U c= U2 by XBOOLE_1:17;

then U c= [#] (M | U2) by PRE_TOPC:def 5;

then reconsider U3 = U as Subset of (M | U2) ;

A13: (M | U2) | U3,((TOP-REAL n) | S2) | (f .: U3) are_homeomorphic by METRIZTS:def 1, A11, METRIZTS:3;

reconsider M2 = M | U2 as non empty SubSpace of M by A9;

reconsider T2 = (TOP-REAL n) | S2 as non empty SubSpace of TOP-REAL n by A10, A9, YELLOW14:18;

reconsider f2 = f as Function of M2,T2 ;

A14: for P being Subset of M2 holds

( P is open iff f2 .: P is open ) by A11, TOPGRP_1:25;

f .: U3 c= [#] ((TOP-REAL n) | S2) ;

then A15: f .: U3 c= S2 by PRE_TOPC:def 5;

A16: X1 in the topology of M by PRE_TOPC:def 2;

U2 = [#] M2 by PRE_TOPC:def 5;

then U3 in the topology of M2 by A16, PRE_TOPC:def 4;

then reconsider S = f .: U3 as open Subset of T2 by A14, PRE_TOPC:def 2;

S in the topology of T2 by PRE_TOPC:def 2;

then consider Q being Subset of (TOP-REAL n) such that

A17: ( Q in the topology of (TOP-REAL n) & S = Q /\ ([#] T2) ) by PRE_TOPC:def 4;

A18: [#] T2 = S2 by PRE_TOPC:def 5;

S2 in the topology of (TOP-REAL n) by PRE_TOPC:def 2;

then S in the topology of (TOP-REAL n) by A18, A17, PRE_TOPC:def 1;

then reconsider S = S as open Subset of (TOP-REAL n) by PRE_TOPC:def 2;

take U ; :: thesis: ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic

take S ; :: thesis: U,S are_homeomorphic

U c= X1 ;

then U c= [#] (M | X1) by PRE_TOPC:def 5;

then reconsider U4 = U as Subset of (M | X1) ;

reconsider U5 = U as Subset of M ;

A19: (M | X1) | U4 = M | U5 by GOBOARD9:2;

(M | U2) | U3 = M | U5 by GOBOARD9:2;

then A20: TopStruct(# the carrier of (X | U), the topology of (X | U) #) = TopStruct(# the carrier of ((M | U2) | U3), the topology of ((M | U2) | U3) #) by A19, A3, PRE_TOPC:36;

((TOP-REAL n) | S2) | (f .: U3) = (TOP-REAL n) | S by A15, PRE_TOPC:7;

hence U,S are_homeomorphic by A13, A20, METRIZTS:def 1; :: thesis: verum

end;p in the carrier of X ;

then reconsider p1 = p as Point of M by A2;

consider U1 being a_neighborhood of p1, S1 being open Subset of (TOP-REAL n) such that

A8: U1,S1 are_homeomorphic by Def4;

consider U2 being open Subset of M, S2 being open Subset of (TOP-REAL n) such that

A9: ( U2 c= U1 & p1 in U2 & U2,S2 are_homeomorphic ) by A8, Th11;

reconsider X2 = X as non empty open SubSpace of M by A1;

reconsider U = U2 /\ X1 as Subset of X2 by XBOOLE_1:17;

A10: M | U2,(TOP-REAL n) | S2 are_homeomorphic by A9, METRIZTS:def 1;

consider f being Function of (M | U2),((TOP-REAL n) | S2) such that

A11: f is being_homeomorphism by T_0TOPSP:def 1, A9, METRIZTS:def 1;

A12: p in U2 /\ X1 by A9, XBOOLE_0:def 4;

U is open by TSEP_1:17;

then reconsider U = U as a_neighborhood of p by A12, CONNSP_2:3;

U c= U2 by XBOOLE_1:17;

then U c= [#] (M | U2) by PRE_TOPC:def 5;

then reconsider U3 = U as Subset of (M | U2) ;

A13: (M | U2) | U3,((TOP-REAL n) | S2) | (f .: U3) are_homeomorphic by METRIZTS:def 1, A11, METRIZTS:3;

reconsider M2 = M | U2 as non empty SubSpace of M by A9;

reconsider T2 = (TOP-REAL n) | S2 as non empty SubSpace of TOP-REAL n by A10, A9, YELLOW14:18;

reconsider f2 = f as Function of M2,T2 ;

A14: for P being Subset of M2 holds

( P is open iff f2 .: P is open ) by A11, TOPGRP_1:25;

f .: U3 c= [#] ((TOP-REAL n) | S2) ;

then A15: f .: U3 c= S2 by PRE_TOPC:def 5;

A16: X1 in the topology of M by PRE_TOPC:def 2;

U2 = [#] M2 by PRE_TOPC:def 5;

then U3 in the topology of M2 by A16, PRE_TOPC:def 4;

then reconsider S = f .: U3 as open Subset of T2 by A14, PRE_TOPC:def 2;

S in the topology of T2 by PRE_TOPC:def 2;

then consider Q being Subset of (TOP-REAL n) such that

A17: ( Q in the topology of (TOP-REAL n) & S = Q /\ ([#] T2) ) by PRE_TOPC:def 4;

A18: [#] T2 = S2 by PRE_TOPC:def 5;

S2 in the topology of (TOP-REAL n) by PRE_TOPC:def 2;

then S in the topology of (TOP-REAL n) by A18, A17, PRE_TOPC:def 1;

then reconsider S = S as open Subset of (TOP-REAL n) by PRE_TOPC:def 2;

take U ; :: thesis: ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic

take S ; :: thesis: U,S are_homeomorphic

U c= X1 ;

then U c= [#] (M | X1) by PRE_TOPC:def 5;

then reconsider U4 = U as Subset of (M | X1) ;

reconsider U5 = U as Subset of M ;

A19: (M | X1) | U4 = M | U5 by GOBOARD9:2;

(M | U2) | U3 = M | U5 by GOBOARD9:2;

then A20: TopStruct(# the carrier of (X | U), the topology of (X | U) #) = TopStruct(# the carrier of ((M | U2) | U3), the topology of ((M | U2) | U3) #) by A19, A3, PRE_TOPC:36;

((TOP-REAL n) | S2) | (f .: U3) = (TOP-REAL n) | S by A15, PRE_TOPC:7;

hence U,S are_homeomorphic by A13, A20, METRIZTS:def 1; :: thesis: verum