let X be TopSpace; :: thesis: for X0 being closed SubSpace of X
for A being Subset of X
for B being Subset of X0 st A = B holds
( B is closed iff A is closed )
let X0 be closed SubSpace of X; :: thesis: for A being Subset of X
for B being Subset of X0 st A = B holds
( B is closed iff A is closed )
let A be Subset of X; :: thesis: for B being Subset of X0 st A = B holds
( B is closed iff A is closed )
let B be Subset of X0; :: thesis: ( A = B implies ( B is closed iff A is closed ) )
assume A1: A = B ; :: thesis: ( B is closed iff A is closed )
reconsider C = the carrier of X0 as Subset of X by Th1;
C is closed by Th11;
hence ( B is closed iff A is closed ) by A1, Th8; :: thesis: verum