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 Th39;

A2: now

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

end;

now

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, Def6;
then ([#] T) \ C in the topology of T by Def5;
then A9: (([#] T) \ C) /\ ([#] X9) in the topology of X9 by Def9;
([#] X9) \ B = ([#] X9) \ C by A8, XBOOLE_1:47
.= ([#] X9) /\ (C ` ) by A1, SUBSET_1:32
.= (([#] T) \ C) /\ ([#] X9) ;
then ([#] X9) \ B is open by A9, Def5;
hence B is closed by Def6; :: 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