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 )

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) ) )

hence Y0 is SubSpace of Y by A9, PRE_TOPC:def 4; :: thesis: verum

( 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 that
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

end;( 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 )

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;( 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

given G being Subset of Y such that A5:
G is open
and
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;( 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

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

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

[#] Y0 c= [#] Y
by A7;
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 )

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;( 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

given G being Subset of Y such that A12:
G in the topology of Y
and
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;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

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

hence Y0 is SubSpace of Y by A9, PRE_TOPC:def 4; :: thesis: verum