let X be non empty SubSpace of M; ( X is open implies ( X is without_boundary & X is n -manifold ) )
assume A1:
X is open
; ( 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
let p be
Point of
X;
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
;
ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic
take
S
;
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;
verum
end;
hence
( X is without_boundary & X is n -manifold )
by Def4; verum