let Y0 be TopStruct ; :: thesis: ( Y0 is SubSpace of Y iff ( the carrier of Y0 c= the carrier of Y & ( for F0 being Subset of Y0 holds

( F0 is closed iff ex F being Subset of Y st

( F is closed & F0 = F /\ 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 F0 being Subset of Y0 holds

( F0 is closed iff ex F being Subset of Y st

( F is closed & F0 = F /\ the carrier of Y0 ) ) ) ) ) :: thesis: ( the carrier of Y0 c= the carrier of Y & ( for F0 being Subset of Y0 holds

( F0 is closed iff ex F being Subset of Y st

( F is closed & F0 = F /\ the carrier of Y0 ) ) ) implies Y0 is SubSpace of Y )

A10: the carrier of Y0 c= the carrier of Y and

A11: for F0 being Subset of Y0 holds

( F0 is closed iff ex F being Subset of Y st

( F is closed & F0 = F /\ the carrier of Y0 ) ) ; :: thesis: Y0 is SubSpace of Y

A12: ([#] Y0) \ ([#] Y) = {} by A10, XBOOLE_1:37;

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

( F0 is closed iff ex F being Subset of Y st

( F is closed & F0 = F /\ 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 F0 being Subset of Y0 holds

( F0 is closed iff ex F being Subset of Y st

( F is closed & F0 = F /\ the carrier of Y0 ) ) ) ) ) :: thesis: ( the carrier of Y0 c= the carrier of Y & ( for F0 being Subset of Y0 holds

( F0 is closed iff ex F being Subset of Y st

( F is closed & F0 = F /\ 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 F0 being Subset of Y0 holds

( F0 is closed iff ex F being Subset of Y st

( F is closed & F0 = F /\ the carrier of Y0 ) ) ) )

hence the carrier of Y0 c= the carrier of Y by A1, PRE_TOPC:def 4; :: thesis: for F0 being Subset of Y0 holds

( F0 is closed iff ex F being Subset of Y st

( F is closed & F0 = F /\ the carrier of Y0 ) )

[#] Y0 c= [#] Y by A2, PRE_TOPC:def 4;

then A3: ([#] Y0) \ ([#] Y) = {} by XBOOLE_1:37;

thus for F0 being Subset of Y0 holds

( F0 is closed iff ex F being Subset of Y st

( F is closed & F0 = F /\ the carrier of Y0 ) ) :: thesis: verum

end;( F0 is closed iff ex F being Subset of Y st

( F is closed & F0 = F /\ the carrier of Y0 ) ) ) )

hence the carrier of Y0 c= the carrier of Y by A1, PRE_TOPC:def 4; :: thesis: for F0 being Subset of Y0 holds

( F0 is closed iff ex F being Subset of Y st

( F is closed & F0 = F /\ the carrier of Y0 ) )

[#] Y0 c= [#] Y by A2, PRE_TOPC:def 4;

then A3: ([#] Y0) \ ([#] Y) = {} by XBOOLE_1:37;

thus for F0 being Subset of Y0 holds

( F0 is closed iff ex F being Subset of Y st

( F is closed & F0 = F /\ the carrier of Y0 ) ) :: thesis: verum

proof

let F0 be Subset of Y0; :: thesis: ( F0 is closed iff ex F being Subset of Y st

( F is closed & F0 = F /\ the carrier of Y0 ) )

set G0 = ([#] Y0) \ F0;

thus ( F0 is closed implies ex F being Subset of Y st

( F is closed & F0 = F /\ the carrier of Y0 ) ) :: thesis: ( ex F being Subset of Y st

( F is closed & F0 = F /\ the carrier of Y0 ) implies F0 is closed )

A8: F0 = F /\ the carrier of Y0 ; :: thesis: F0 is closed

hence F0 is closed by PRE_TOPC:def 3; :: thesis: verum

end;( F is closed & F0 = F /\ the carrier of Y0 ) )

set G0 = ([#] Y0) \ F0;

thus ( F0 is closed implies ex F being Subset of Y st

( F is closed & F0 = F /\ the carrier of Y0 ) ) :: thesis: ( ex F being Subset of Y st

( F is closed & F0 = F /\ the carrier of Y0 ) implies F0 is closed )

proof

given F being Subset of Y such that A7:
F is closed
and
assume
F0 is closed
; :: thesis: ex F being Subset of Y st

( F is closed & F0 = F /\ the carrier of Y0 )

then ([#] Y0) \ F0 is open by PRE_TOPC:def 3;

then consider G being Subset of Y such that

A4: G is open and

A5: ([#] Y0) \ F0 = G /\ the carrier of Y0 by A2, Def1;

take F = ([#] Y) \ G; :: thesis: ( F is closed & F0 = F /\ the carrier of Y0 )

A6: G = ([#] Y) \ F by PRE_TOPC:3;

hence F is closed by A4, PRE_TOPC:def 3; :: thesis: F0 = F /\ the carrier of Y0

F0 = ([#] Y0) \ (G /\ the carrier of Y0) by A5, PRE_TOPC:3

.= (([#] Y0) \ G) \/ (([#] Y0) \ the carrier of Y0) by XBOOLE_1:54

.= (([#] Y0) \ G) \/ {} by XBOOLE_1:37

.= (([#] Y0) \ ([#] Y)) \/ (([#] Y0) /\ F) by A6, XBOOLE_1:52

.= ([#] Y0) /\ F by A3 ;

hence F0 = F /\ the carrier of Y0 ; :: thesis: verum

end;( F is closed & F0 = F /\ the carrier of Y0 )

then ([#] Y0) \ F0 is open by PRE_TOPC:def 3;

then consider G being Subset of Y such that

A4: G is open and

A5: ([#] Y0) \ F0 = G /\ the carrier of Y0 by A2, Def1;

take F = ([#] Y) \ G; :: thesis: ( F is closed & F0 = F /\ the carrier of Y0 )

A6: G = ([#] Y) \ F by PRE_TOPC:3;

hence F is closed by A4, PRE_TOPC:def 3; :: thesis: F0 = F /\ the carrier of Y0

F0 = ([#] Y0) \ (G /\ the carrier of Y0) by A5, PRE_TOPC:3

.= (([#] Y0) \ G) \/ (([#] Y0) \ the carrier of Y0) by XBOOLE_1:54

.= (([#] Y0) \ G) \/ {} by XBOOLE_1:37

.= (([#] Y0) \ ([#] Y)) \/ (([#] Y0) /\ F) by A6, XBOOLE_1:52

.= ([#] Y0) /\ F by A3 ;

hence F0 = F /\ the carrier of Y0 ; :: thesis: verum

A8: F0 = F /\ the carrier of Y0 ; :: thesis: F0 is closed

now :: thesis: ex G being Element of K19( the carrier of Y) st

( G is open & ([#] Y0) \ F0 = G /\ the carrier of Y0 )

then
([#] Y0) \ F0 is open
by A2, Def1;( G is open & ([#] Y0) \ F0 = G /\ the carrier of Y0 )

take G = ([#] Y) \ F; :: thesis: ( G is open & ([#] Y0) \ F0 = G /\ the carrier of Y0 )

A9: F = ([#] Y) \ G by PRE_TOPC:3;

thus G is open by A7, PRE_TOPC:def 3; :: thesis: ([#] Y0) \ F0 = G /\ the carrier of Y0

([#] Y0) \ F0 = (([#] Y0) \ F) \/ (([#] Y0) \ the carrier of Y0) by A8, XBOOLE_1:54

.= (([#] Y0) \ F) \/ {} by XBOOLE_1:37

.= (([#] Y0) \ ([#] Y)) \/ (([#] Y0) /\ G) by A9, XBOOLE_1:52

.= ([#] Y0) /\ G by A3 ;

hence ([#] Y0) \ F0 = G /\ the carrier of Y0 ; :: thesis: verum

end;A9: F = ([#] Y) \ G by PRE_TOPC:3;

thus G is open by A7, PRE_TOPC:def 3; :: thesis: ([#] Y0) \ F0 = G /\ the carrier of Y0

([#] Y0) \ F0 = (([#] Y0) \ F) \/ (([#] Y0) \ the carrier of Y0) by A8, XBOOLE_1:54

.= (([#] Y0) \ F) \/ {} by XBOOLE_1:37

.= (([#] Y0) \ ([#] Y)) \/ (([#] Y0) /\ G) by A9, XBOOLE_1:52

.= ([#] Y0) /\ G by A3 ;

hence ([#] Y0) \ F0 = G /\ the carrier of Y0 ; :: thesis: verum

hence F0 is closed by PRE_TOPC:def 3; :: thesis: verum

A10: the carrier of Y0 c= the carrier of Y and

A11: for F0 being Subset of Y0 holds

( F0 is closed iff ex F being Subset of Y st

( F is closed & F0 = F /\ the carrier of Y0 ) ) ; :: thesis: Y0 is SubSpace of Y

A12: ([#] Y0) \ ([#] Y) = {} by A10, XBOOLE_1:37;

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

proof

hence
Y0 is SubSpace of Y
by A10, Def1; :: thesis: verum
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 ) )

set F0 = ([#] Y0) \ G0;

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 )

A18: G0 = G /\ the carrier of Y0 ; :: thesis: G0 is open

hence G0 is open by PRE_TOPC:def 3; :: thesis: verum

end;( G is open & G0 = G /\ the carrier of Y0 ) )

set F0 = ([#] Y0) \ G0;

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 A17:
G is open
and
set F0 = ([#] Y0) \ G0;

A13: G0 = ([#] Y0) \ (([#] Y0) \ G0) by PRE_TOPC:3;

assume G0 is open ; :: thesis: ex G being Subset of Y st

( G is open & G0 = G /\ the carrier of Y0 )

then ([#] Y0) \ G0 is closed by A13, PRE_TOPC:def 3;

then consider F being Subset of Y such that

A14: F is closed and

A15: ([#] Y0) \ G0 = F /\ the carrier of Y0 by A11;

take G = ([#] Y) \ F; :: thesis: ( G is open & G0 = G /\ the carrier of Y0 )

thus G is open by A14, PRE_TOPC:def 3; :: thesis: G0 = G /\ the carrier of Y0

A16: F = ([#] Y) \ G by PRE_TOPC:3;

G0 = (([#] Y0) \ F) \/ (([#] Y0) \ the carrier of Y0) by A13, A15, XBOOLE_1:54

.= (([#] Y0) \ F) \/ {} by XBOOLE_1:37

.= (([#] Y0) \ ([#] Y)) \/ (([#] Y0) /\ G) by A16, XBOOLE_1:52

.= ([#] Y0) /\ G by A12 ;

hence G0 = G /\ the carrier of Y0 ; :: thesis: verum

end;A13: G0 = ([#] Y0) \ (([#] Y0) \ G0) by PRE_TOPC:3;

assume G0 is open ; :: thesis: ex G being Subset of Y st

( G is open & G0 = G /\ the carrier of Y0 )

then ([#] Y0) \ G0 is closed by A13, PRE_TOPC:def 3;

then consider F being Subset of Y such that

A14: F is closed and

A15: ([#] Y0) \ G0 = F /\ the carrier of Y0 by A11;

take G = ([#] Y) \ F; :: thesis: ( G is open & G0 = G /\ the carrier of Y0 )

thus G is open by A14, PRE_TOPC:def 3; :: thesis: G0 = G /\ the carrier of Y0

A16: F = ([#] Y) \ G by PRE_TOPC:3;

G0 = (([#] Y0) \ F) \/ (([#] Y0) \ the carrier of Y0) by A13, A15, XBOOLE_1:54

.= (([#] Y0) \ F) \/ {} by XBOOLE_1:37

.= (([#] Y0) \ ([#] Y)) \/ (([#] Y0) /\ G) by A16, XBOOLE_1:52

.= ([#] Y0) /\ G by A12 ;

hence G0 = G /\ the carrier of Y0 ; :: thesis: verum

A18: G0 = G /\ the carrier of Y0 ; :: thesis: G0 is open

now :: thesis: ex F being Element of K19( the carrier of Y) st

( F is closed & ([#] Y0) \ G0 = F /\ the carrier of Y0 )

then
( G0 = ([#] Y0) \ (([#] Y0) \ G0) & ([#] Y0) \ G0 is closed )
by A11, PRE_TOPC:3;( F is closed & ([#] Y0) \ G0 = F /\ the carrier of Y0 )

take F = ([#] Y) \ G; :: thesis: ( F is closed & ([#] Y0) \ G0 = F /\ the carrier of Y0 )

A19: G = ([#] Y) \ F by PRE_TOPC:3;

hence F is closed by A17, PRE_TOPC:def 3; :: thesis: ([#] Y0) \ G0 = F /\ the carrier of Y0

([#] Y0) \ G0 = (([#] Y0) \ G) \/ (([#] Y0) \ the carrier of Y0) by A18, XBOOLE_1:54

.= (([#] Y0) \ G) \/ {} by XBOOLE_1:37

.= (([#] Y0) \ ([#] Y)) \/ (([#] Y0) /\ F) by A19, XBOOLE_1:52

.= ([#] Y0) /\ F by A12 ;

hence ([#] Y0) \ G0 = F /\ the carrier of Y0 ; :: thesis: verum

end;A19: G = ([#] Y) \ F by PRE_TOPC:3;

hence F is closed by A17, PRE_TOPC:def 3; :: thesis: ([#] Y0) \ G0 = F /\ the carrier of Y0

([#] Y0) \ G0 = (([#] Y0) \ G) \/ (([#] Y0) \ the carrier of Y0) by A18, XBOOLE_1:54

.= (([#] Y0) \ G) \/ {} by XBOOLE_1:37

.= (([#] Y0) \ ([#] Y)) \/ (([#] Y0) /\ F) by A19, XBOOLE_1:52

.= ([#] Y0) /\ F by A12 ;

hence ([#] Y0) \ G0 = F /\ the carrier of Y0 ; :: thesis: verum

hence G0 is open by PRE_TOPC:def 3; :: thesis: verum