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

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