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

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

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 open )
assume A1: B = the carrier of X2 ; :: thesis: B is open
then reconsider BB = B as Subset of X1 by BORSUK_1:1;
BB is open by A1, Def1;
then A2: ex A being Subset of X st
( A is open & A /\ ([#] X1) = BB ) by TOPS_2:24;
C is open by Def1;
hence B is open by A2; :: thesis: verum

end;

hence X2 is open SubSpace of X by Def1, Th7; :: thesis: verum