let X be TopSpace; :: thesis: for X1 being closed SubSpace of X
for X2 being closed SubSpace of X1 holds X2 is closed SubSpace of X
let X1 be closed SubSpace of X; :: thesis: for X2 being closed SubSpace of X1 holds X2 is closed SubSpace of X
let X2 be closed SubSpace of X1; :: thesis: X2 is closed SubSpace of X

now :: thesis: for B being Subset of X st B = the carrier of X2 holds
B is closed

reconsider C = [#] X1 as Subset of X by BORSUK_1:1;
let B be Subset of X; :: thesis: ( B = the carrier of X2 implies B is closed )
assume A1: B = the carrier of X2 ; :: thesis: B is closed
then reconsider BB = B as Subset of X1 by BORSUK_1:1;
BB is closed by A1, BORSUK_1:def 11;
then A2: ex A being Subset of X st
( A is closed & A /\ ([#] X1) = BB ) by PRE_TOPC:13;
C is closed by BORSUK_1:def 11;
hence B is closed by A2; :: thesis: verum

end;

hence X2 is closed SubSpace of X by Th7, BORSUK_1:def 11; :: thesis: verum