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