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

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