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 10;
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:8;
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

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, RELAT_1:71;
assume P is open ; :: thesis: (h " ) " P is open
then A8: P in the topology of X by PRE_TOPC:def 5;
(h " ) " P = h .: Q by A2, A3, TOPS_2:67
.= Q by A2, FUNCT_1:162 ;
hence (h " ) " P in the topology of (Y | (rng (incl X,Y))) by A5, A6, A2, A8, RELAT_1:71; :: according to PRE_TOPC:def 5 :: thesis: verum

end;

A9: ( [#] X = {} implies [#] X = {} ) ;
A10: for P being Subset of (Y | (rng (incl X,Y))) st P is open holds
h " P is open

proof

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, RELAT_1:71;
assume P is open ; :: thesis: h " P is open
then P in the topology of (Y | (rng (incl X,Y))) by PRE_TOPC:def 5;
then Q in the topology of X by A5, A6, A2, RELAT_1:71;
then Q is open by PRE_TOPC:def 5;
then (id X) " Q is open by A9, TOPS_2:55;
then (id X) " Q in the topology of X by PRE_TOPC:def 5;
hence h " P in the topology of X by A1, YELLOW_9:def 1; :: according to PRE_TOPC:def 5 :: thesis: verum

end;

take h ; :: according to COMPACT1:def 7 :: thesis: ( h = incl X,Y & h is being_homeomorphism )
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 10; :: 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, RELAT_1:71;
hence h is continuous by A10, TOPS_2:55; :: thesis: h " is continuous
( [#] X = {} implies [#] (Y | (rng (incl X,Y))) = {} ) by A2, A3, RELAT_1:71;
hence h " is continuous by A7, TOPS_2:55; :: thesis: verum