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