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