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 ;
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 () st U,S are_homeomorphic
proof
let p be Point of X; :: thesis: ex U being a_neighborhood of p ex S being open Subset of () 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 () such that
A8: U1,S1 are_homeomorphic by Def4;
consider U2 being open Subset of M, S2 being open Subset of () such that
A9: ( U2 c= U1 & p1 in U2 & U2,S2 are_homeomorphic ) by ;
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,() | S2 are_homeomorphic by ;
consider f being Function of (M | U2),(() | S2) such that
A11: f is being_homeomorphism by ;
A12: p in U2 /\ X1 by ;
U is open by TSEP_1:17;
then reconsider U = U as a_neighborhood of p by ;
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,(() | S2) | (f .: U3) are_homeomorphic by ;
reconsider M2 = M | U2 as non empty SubSpace of M by A9;
reconsider T2 = () | S2 as non empty SubSpace of TOP-REAL n by ;
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 ;
f .: U3 c= [#] (() | 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 ;
then reconsider S = f .: U3 as open Subset of T2 by ;
S in the topology of T2 by PRE_TOPC:def 2;
then consider Q being Subset of () such that
A17: ( Q in the topology of () & S = Q /\ ([#] T2) ) by PRE_TOPC:def 4;
A18: [#] T2 = S2 by PRE_TOPC:def 5;
S2 in the topology of () by PRE_TOPC:def 2;
then S in the topology of () by ;
then reconsider S = S as open Subset of () by PRE_TOPC:def 2;
take U ; :: thesis: ex S being open Subset of () st U,S are_homeomorphic
take S ; :: thesis:
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 ;
((TOP-REAL n) | S2) | (f .: U3) = () | S by ;
hence U,S are_homeomorphic by ; :: thesis: verum
end;
hence ( X is without_boundary & X is n -manifold ) by Def4; :: thesis: verum