let Y be TopStruct ; :: thesis: for Y0 being SubSpace of Y
for F being Subset of st F is closed holds
ex F0 being Subset of st
( F0 is closed & F0 = F /\ the carrier of Y0 )
let Y0 be SubSpace of Y; :: thesis: for F being Subset of st F is closed holds
ex F0 being Subset of st
( F0 is closed & F0 = F /\ the carrier of Y0 )
let F be Subset of ; :: thesis: ( F is closed implies ex F0 being Subset of st
( F0 is closed & F0 = F /\ the carrier of Y0 ) )
assume A1: F is closed ; :: thesis: ex F0 being Subset of 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 by PRE_TOPC:def 9;
reconsider F0 = F /\ A as Subset of 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