let X, Y be TopSpace; :: thesis: ( [#] X c= [#] Y & ex Xy being Subset of Y st

( Xy = [#] X & the topology of (Y | Xy) = the topology of X ) implies incl (X,Y) is embedding )

assume A1: [#] X c= [#] Y ; :: thesis: ( for Xy being Subset of Y holds

( not Xy = [#] X or not the topology of (Y | Xy) = the topology of X ) or incl (X,Y) is embedding )

A2: incl (X,Y) = id X by A1, YELLOW_9:def 1;

set YY = Y | (rng (incl (X,Y)));

A3: [#] (Y | (rng (incl (X,Y)))) = rng (incl (X,Y)) by PRE_TOPC:def 5;

A4: ( [#] Y = {} implies [#] X = {} ) by A1;

then reconsider h = incl (X,Y) as Function of X,(Y | (rng (incl (X,Y)))) by A3, FUNCT_2:6;

set f = id X;

given Xy being Subset of Y such that A5: Xy = [#] X and

A6: the topology of (Y | Xy) = the topology of X ; :: thesis: incl (X,Y) is embedding

A7: for P being Subset of X st P is open holds

(h ") " P is open

A10: for P being Subset of (Y | (rng (incl (X,Y)))) st P is open holds

h " P is open

thus h = incl (X,Y) ; :: thesis: h is being_homeomorphism

thus ( dom h = [#] X & rng h = [#] (Y | (rng (incl (X,Y)))) ) by A4, FUNCT_2:def 1, PRE_TOPC:def 5; :: according to TOPS_2:def 5 :: thesis: ( h is one-to-one & h is continuous & h " is continuous )

thus h is one-to-one by A2; :: thesis: ( h is continuous & h " is continuous )

( [#] (Y | (rng (incl (X,Y)))) = {} implies [#] X = {} ) by A2, A3;

hence h is continuous by A10, TOPS_2:43; :: thesis: h " is continuous

( [#] X = {} implies [#] (Y | (rng (incl (X,Y)))) = {} ) ;

hence h " is continuous by A7, TOPS_2:43; :: thesis: verum

( Xy = [#] X & the topology of (Y | Xy) = the topology of X ) implies incl (X,Y) is embedding )

assume A1: [#] X c= [#] Y ; :: thesis: ( for Xy being Subset of Y holds

( not Xy = [#] X or not the topology of (Y | Xy) = the topology of X ) or incl (X,Y) is embedding )

A2: incl (X,Y) = id X by A1, YELLOW_9:def 1;

set YY = Y | (rng (incl (X,Y)));

A3: [#] (Y | (rng (incl (X,Y)))) = rng (incl (X,Y)) by PRE_TOPC:def 5;

A4: ( [#] Y = {} implies [#] X = {} ) by A1;

then reconsider h = incl (X,Y) as Function of X,(Y | (rng (incl (X,Y)))) by A3, FUNCT_2:6;

set f = id X;

given Xy being Subset of Y such that A5: Xy = [#] X and

A6: the topology of (Y | Xy) = the topology of X ; :: thesis: incl (X,Y) is embedding

A7: for P being Subset of X st P is open holds

(h ") " P is open

proof

A9:
( [#] X = {} implies [#] X = {} )
;
let P be Subset of X; :: thesis: ( P is open implies (h ") " P is open )

reconsider Q = P as Subset of (Y | (rng (incl (X,Y)))) by A2, A3;

assume P is open ; :: thesis: (h ") " P is open

then A8: P in the topology of X ;

(h ") " P = h .: Q by A2, A3, TOPS_2:54

.= Q by A2, FUNCT_1:92 ;

hence (h ") " P in the topology of (Y | (rng (incl (X,Y)))) by A5, A6, A2, A8; :: according to PRE_TOPC:def 2 :: thesis: verum

end;reconsider Q = P as Subset of (Y | (rng (incl (X,Y)))) by A2, A3;

assume P is open ; :: thesis: (h ") " P is open

then A8: P in the topology of X ;

(h ") " P = h .: Q by A2, A3, TOPS_2:54

.= Q by A2, FUNCT_1:92 ;

hence (h ") " P in the topology of (Y | (rng (incl (X,Y)))) by A5, A6, A2, A8; :: according to PRE_TOPC:def 2 :: thesis: verum

A10: for P being Subset of (Y | (rng (incl (X,Y)))) st P is open holds

h " P is open

proof

take
h
; :: according to COMPACT1:def 7 :: thesis: ( h = incl (X,Y) & h is being_homeomorphism )
let P be Subset of (Y | (rng (incl (X,Y)))); :: thesis: ( P is open implies h " P is open )

reconsider Q = P as Subset of X by A2, A3;

assume P is open ; :: thesis: h " P is open

then P in the topology of (Y | (rng (incl (X,Y)))) ;

then Q in the topology of X by A5, A6, A2;

then Q is open ;

then (id X) " Q is open by A9, TOPS_2:43;

then (id X) " Q in the topology of X ;

hence h " P in the topology of X by A1, YELLOW_9:def 1; :: according to PRE_TOPC:def 2 :: thesis: verum

end;reconsider Q = P as Subset of X by A2, A3;

assume P is open ; :: thesis: h " P is open

then P in the topology of (Y | (rng (incl (X,Y)))) ;

then Q in the topology of X by A5, A6, A2;

then Q is open ;

then (id X) " Q is open by A9, TOPS_2:43;

then (id X) " Q in the topology of X ;

hence h " P in the topology of X by A1, YELLOW_9:def 1; :: according to PRE_TOPC:def 2 :: thesis: verum

thus h = incl (X,Y) ; :: thesis: h is being_homeomorphism

thus ( dom h = [#] X & rng h = [#] (Y | (rng (incl (X,Y)))) ) by A4, FUNCT_2:def 1, PRE_TOPC:def 5; :: according to TOPS_2:def 5 :: thesis: ( h is one-to-one & h is continuous & h " is continuous )

thus h is one-to-one by A2; :: thesis: ( h is continuous & h " is continuous )

( [#] (Y | (rng (incl (X,Y)))) = {} implies [#] X = {} ) by A2, A3;

hence h is continuous by A10, TOPS_2:43; :: thesis: h " is continuous

( [#] X = {} implies [#] (Y | (rng (incl (X,Y)))) = {} ) ;

hence h " is continuous by A7, TOPS_2:43; :: thesis: verum