let Y be TopStruct ; :: thesis: for Y0 being SubSpace of Y
for G being Subset of st G is open holds
ex G0 being Subset of st
( G0 is open & G0 = G /\ the carrier of Y0 )
let Y0 be SubSpace of Y; :: thesis: for G being Subset of st G is open holds
ex G0 being Subset of st
( G0 is open & G0 = G /\ the carrier of Y0 )
let G be Subset of ; :: thesis: ( G is open implies ex G0 being Subset of st
( G0 is open & G0 = G /\ the carrier of Y0 ) )
assume A1: G is open ; :: thesis: ex G0 being Subset of st
( G0 is open & G0 = G /\ 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 G0 = G /\ A as Subset of by XBOOLE_1:17;
take G0 ; :: thesis: ( G0 is open & G0 = G /\ the carrier of Y0 )
thus G0 is open by A1, Def1; :: thesis: G0 = G /\ the carrier of Y0
thus G0 = G /\ the carrier of Y0 ; :: thesis: verum