let M be non empty MetrSpace; :: thesis: for P being Subset of (TopSpaceMetr M)
for Q being non empty Subset of M st P = Q holds
(TopSpaceMetr M) | P = TopSpaceMetr (M | Q)
let P be Subset of (TopSpaceMetr M); :: thesis: for Q being non empty Subset of M st P = Q holds
(TopSpaceMetr M) | P = TopSpaceMetr (M | Q)
let Q be non empty Subset of M; :: thesis: ( P = Q implies (TopSpaceMetr M) | P = TopSpaceMetr (M | Q) )
reconsider N = TopSpaceMetr (M | Q) as SubSpace of TopSpaceMetr M by TOPMETR:13;
A1: the carrier of N = the carrier of (M | Q) by TOPMETR:12;
assume P = Q ; :: thesis: (TopSpaceMetr M) | P = TopSpaceMetr (M | Q)
then [#] N = P by A1, TOPMETR:def 2;
hence (TopSpaceMetr M) | P = TopSpaceMetr (M | Q) by PRE_TOPC:def 5; :: thesis: verum