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 A = B ; :: thesis: T | A = S | B
then ( S | B is SubSpace of T & [#] (S | B) = A ) by PRE_TOPC:def 5, TSEP_1:7;
hence T | A = S | B by PRE_TOPC:def 5; :: thesis: verum