let T be TopStruct ; :: thesis: for X9 being SubSpace of T
for B being Subset of X9 holds
( B is closed iff ex C being Subset of T st
( C is closed & C /\ ([#] X9) = B ) )
let X9 be SubSpace of T; :: thesis: for B being Subset of X9 holds
( B is closed iff ex C being Subset of T st
( C is closed & C /\ ([#] X9) = B ) )
let B be Subset of X9; :: thesis: ( B is closed iff ex C being Subset of T st
( C is closed & C /\ ([#] X9) = B ) )
A1: [#] X9 is Subset of T by Th11;

A2: now :: thesis: ( B is closed implies ex C being Subset of T st
( C is closed & C /\ ([#] X9) = B ) )

assume B is closed ; :: thesis: ex C being Subset of T st
( C is closed & C /\ ([#] X9) = B )
then ([#] X9) \ B is open ;
then ([#] X9) \ B in the topology of X9 ;
then consider V being Subset of T such that
A3: V in the topology of T and
A4: ([#] X9) \ B = V /\ ([#] X9) by Def4;
A5: (([#] T) \ V) /\ ([#] X9) = ([#] X9) /\ (V `)
.= ([#] X9) \ V by A1, SUBSET_1:13
.= ([#] X9) \ (([#] X9) /\ V) by XBOOLE_1:47
.= B by A4, Th3 ;
reconsider V1 = V as Subset of T ;
A6: ([#] T) \ (([#] T) \ V) = V by Th3;
V1 is open by A3;
then ([#] T) \ V is closed by A6;
hence ex C being Subset of T st
( C is closed & C /\ ([#] X9) = B ) by A5; :: thesis: verum

end;

now :: thesis: ( ex C being Subset of T st
( C is closed & C /\ ([#] X9) = B ) implies B is closed )

given C being Subset of T such that A7: C is closed and
A8: C /\ ([#] X9) = B ; :: thesis: B is closed
([#] T) \ C is open by A7;
then ([#] T) \ C in the topology of T ;
then A9: (([#] T) \ C) /\ ([#] X9) in the topology of X9 by Def4;
([#] X9) \ B = ([#] X9) \ C by A8, XBOOLE_1:47
.= ([#] X9) /\ (C `) by A1, SUBSET_1:13
.= (([#] T) \ C) /\ ([#] X9) ;
then ([#] X9) \ B is open by A9;
hence B is closed ; :: thesis: verum

end;

hence ( B is closed iff ex C being Subset of T st
( C is closed & C /\ ([#] X9) = B ) ) by A2; :: thesis: verum