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 ; :: 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 ;
reconsider G = G as Subset of Y ;
take G ; :: thesis: ( G is open & G0 = G /\ the carrier of Y0 )
thus G is open by ; :: 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 ;
then G0 in the topology of Y0 by ;
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 ; :: 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 ;
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 ; :: thesis: verum