let Y0 be TopStruct ; :: thesis:
A1: ( [#] Y0 = the carrier of Y0 & [#] Y = the carrier of Y ) ;
thus ( Y0 is SubSpace of Y implies ( the carrier of Y0 c= the carrier of Y & ( for G0 being Subset of Y0 holds
( G0 is open iff ex G being Subset of Y st
( G is open & G0 = G /\ the carrier of Y0 ) ) ) ) ) :: thesis:

assume A2: Y0 is SubSpace of Y ; :: thesis:
hence the carrier of Y0 c= the carrier of Y by A1, PRE_TOPC:def 4; :: thesis:
thus for G0 being Subset of Y0 holds
( G0 is open iff ex G being Subset of Y st
( G is open & G0 = G /\ the carrier of Y0 ) ) :: thesis:

let G0 be Subset of Y0; :: thesis:
thus ( G0 is open implies ex G being Subset of Y st
( G is open & G0 = G /\ the carrier of Y0 ) ) :: thesis:

assume G0 is open ; :: thesis:
then G0 in the topology of Y0 by PRE_TOPC:def 2;
then consider G being Subset of Y such that
A3: G in the topology of Y and
A4: G0 = G /\ ([#] Y0) by A2, PRE_TOPC:def 4;
reconsider G = G as Subset of Y ;
take G ; :: thesis:
thus G is open by A3, PRE_TOPC:def 2; :: thesis:
thus G0 = G /\ the carrier of Y0 by A4; :: thesis:

end;

end;

assume that
A7: the carrier of Y0 c= the carrier of Y and
A8: for G0 being Subset of Y0 holds
( G0 is open iff ex G being Subset of Y st
( G is open & G0 = G /\ the carrier of Y0 ) ) ; :: thesis:
A9: for G0 being Subset of Y0 holds
( G0 in the topology of Y0 iff ex G being Subset of Y st
( G in the topology of Y & G0 = G /\ ([#] Y0) ) )

let G0 be Subset of Y0; :: thesis:
reconsider M = G0 as Subset of Y0 ;
thus ( G0 in the topology of Y0 implies ex G being Subset of Y st
( G in the topology of Y & G0 = G /\ ([#] Y0) ) ) :: thesis:

reconsider M = G0 as Subset of Y0 ;
assume G0 in the topology of Y0 ; :: thesis:
then M is open by PRE_TOPC:def 2;
then consider G being Subset of Y such that
A10: G is open and
A11: G0 = G /\ the carrier of Y0 by A8;
take G ; :: thesis:
thus G in the topology of Y by A10, PRE_TOPC:def 2; :: thesis:
thus G0 = G /\ ([#] Y0) by A11; :: thesis:

end;

given G being Subset of Y such that A12: G in the topology of Y and
A13: G0 = G /\ ([#] Y0) ; :: thesis:
reconsider G = G as Subset of Y ;
( G is open & G0 = G /\ the carrier of Y0 ) by A13, A12, PRE_TOPC:def 2;
then M is open by A8;
hence G0 in the topology of Y0 by PRE_TOPC:def 2; :: thesis:

end;