let Y0 be TopStruct ; :: thesis: ( Y0 is SubSpace of Y iff ( 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 ) ) ) ) )
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: ( 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 ) ) ) implies Y0 is SubSpace of Y )

proof

assume A2: Y0 is SubSpace of Y ; :: thesis: ( 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 ) ) ) )
hence the carrier of Y0 c= the carrier of Y by A1, PRE_TOPC:def 4; :: thesis: 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 ) )
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: verum

proof

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

proof

assume G0 is open ; :: thesis: ex G being Subset of Y st
( G is open & G0 = G /\ the carrier of Y0 )
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: ( G is open & G0 = G /\ the carrier of Y0 )
thus G is open by A3, PRE_TOPC:def 2; :: thesis: G0 = G /\ the carrier of Y0
thus G0 = G /\ the carrier of Y0 by A4; :: thesis: verum

end;

given G being Subset of Y such that A5: G is open and
A6: G0 = G /\ the carrier of Y0 ; :: thesis: G0 is open
( G in the topology of Y & G0 = G /\ ([#] Y0) ) by A6, A5, PRE_TOPC:def 2;
then G0 in the topology of Y0 by A2, PRE_TOPC:def 4;
hence G0 is open by PRE_TOPC:def 2; :: thesis: verum

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: Y0 is SubSpace of Y
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) ) )

proof

let G0 be Subset of Y0; :: thesis: ( G0 in the topology of Y0 iff ex G being Subset of Y st
( G in the topology of Y & G0 = G /\ ([#] Y0) ) )
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: ( ex G being Subset of Y st
( G in the topology of Y & G0 = G /\ ([#] Y0) ) implies G0 in the topology of Y0 )

proof

reconsider M = G0 as Subset of Y0 ;
assume G0 in the topology of Y0 ; :: thesis: ex G being Subset of Y st
( G in the topology of Y & G0 = G /\ ([#] Y0) )
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: ( G in the topology of Y & G0 = G /\ ([#] Y0) )
thus G in the topology of Y by A10, PRE_TOPC:def 2; :: thesis: G0 = G /\ ([#] Y0)
thus G0 = G /\ ([#] Y0) by A11; :: thesis: verum

end;

given G being Subset of Y such that A12: G in the topology of Y and
A13: G0 = G /\ ([#] Y0) ; :: thesis: G0 in the topology of Y0
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: verum

end;

[#] Y0 c= [#] Y by A7;
hence Y0 is SubSpace of Y by A9, PRE_TOPC:def 4; :: thesis: verum