let n be Nat; :: thesis: for P being Subset of (TOP-REAL n)
for Q being non empty Subset of (Euclid n) st P = Q holds
(TOP-REAL n) | P = TopSpaceMetr ((Euclid n) | Q)
let P be Subset of (TOP-REAL n); :: thesis: for Q being non empty Subset of (Euclid n) st P = Q holds
(TOP-REAL n) | P = TopSpaceMetr ((Euclid n) | Q)
let Q be non empty Subset of (Euclid n); :: thesis: ( P = Q implies (TOP-REAL n) | P = TopSpaceMetr ((Euclid n) | Q) )
set M = TopSpaceMetr ((Euclid n) | Q);
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by Def8;
then TopSpaceMetr ((Euclid n) | Q) is SubSpace of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) by TOPMETR:13;
then reconsider M = TopSpaceMetr ((Euclid n) | Q) as SubSpace of TOP-REAL n by PRE_TOPC:29;
assume P = Q ; :: thesis: (TOP-REAL n) | P = TopSpaceMetr ((Euclid n) | Q)
then [#] M = P by TOPMETR:def 2;
hence (TOP-REAL n) | P = TopSpaceMetr ((Euclid n) | Q) by PRE_TOPC:def 5; :: thesis: verum