let T be TopSpace; :: thesis: for A, B being Subset of T
for F being Subset of (T | A) st F = B holds
(T | A) | F = T | B
let A, B be Subset of T; :: thesis: for F being Subset of (T | A) st F = B holds
(T | A) | F = T | B
let F be Subset of (T | A); :: thesis: ( F = B implies (T | A) | F = T | B )
assume A1: F = B ; :: thesis: (T | A) | F = T | B
( (T | A) | F is SubSpace of T & [#] ((T | A) | F) = F ) by PRE_TOPC:def 5, TSEP_1:7;
hence (T | A) | F = T | B by A1, PRE_TOPC:def 5; :: thesis: verum