theorem Th3: :: COMPACT1:3

for X, Y being TopSpace st [#] X c= [#] Y & ex Xy being Subset of Y st
( Xy = [#] X & the topology of (Y | Xy) = the topology of X ) holds
incl (X,Y) is embedding