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 )

proof

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

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 )

proof

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;

given F being Subset of Y such that A7: F is closed and
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 )

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;

then ([#] Y0) \ F0 is open by A2, Def1;
hence F0 is closed by PRE_TOPC:def 3; :: thesis: verum

end;

end;

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

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 )

proof

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;

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

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;

then ( G0 = ([#] Y0) \ (([#] Y0) \ G0) & ([#] Y0) \ G0 is closed ) by A11, PRE_TOPC:3;
hence G0 is open by PRE_TOPC:def 3; :: thesis: verum

end;

hence Y0 is SubSpace of Y by A10, Def1; :: thesis: verum