let Y be TopStruct ; :: thesis: for Y0 being SubSpace of Y

for F being Subset of Y st F is closed holds

ex F0 being Subset of Y0 st

( F0 is closed & F0 = F /\ the carrier of Y0 )

let Y0 be SubSpace of Y; :: thesis: for F being Subset of Y st F is closed holds

ex F0 being Subset of Y0 st

( F0 is closed & F0 = F /\ the carrier of Y0 )

let F be Subset of Y; :: thesis: ( F is closed implies ex F0 being Subset of Y0 st

( F0 is closed & F0 = F /\ the carrier of Y0 ) )

assume A1: F is closed ; :: thesis: ex F0 being Subset of Y0 st

( F0 is closed & F0 = F /\ the carrier of Y0 )

( [#] Y0 = the carrier of Y0 & [#] Y = the carrier of Y ) ;

then reconsider A = the carrier of Y0 as Subset of Y by PRE_TOPC:def 4;

reconsider F0 = F /\ A as Subset of Y0 by XBOOLE_1:17;

take F0 ; :: thesis: ( F0 is closed & F0 = F /\ the carrier of Y0 )

thus F0 is closed by A1, Def2; :: thesis: F0 = F /\ the carrier of Y0

thus F0 = F /\ the carrier of Y0 ; :: thesis: verum

for F being Subset of Y st F is closed holds

ex F0 being Subset of Y0 st

( F0 is closed & F0 = F /\ the carrier of Y0 )

let Y0 be SubSpace of Y; :: thesis: for F being Subset of Y st F is closed holds

ex F0 being Subset of Y0 st

( F0 is closed & F0 = F /\ the carrier of Y0 )

let F be Subset of Y; :: thesis: ( F is closed implies ex F0 being Subset of Y0 st

( F0 is closed & F0 = F /\ the carrier of Y0 ) )

assume A1: F is closed ; :: thesis: ex F0 being Subset of Y0 st

( F0 is closed & F0 = F /\ the carrier of Y0 )

( [#] Y0 = the carrier of Y0 & [#] Y = the carrier of Y ) ;

then reconsider A = the carrier of Y0 as Subset of Y by PRE_TOPC:def 4;

reconsider F0 = F /\ A as Subset of Y0 by XBOOLE_1:17;

take F0 ; :: thesis: ( F0 is closed & F0 = F /\ the carrier of Y0 )

thus F0 is closed by A1, Def2; :: thesis: F0 = F /\ the carrier of Y0

thus F0 = F /\ the carrier of Y0 ; :: thesis: verum