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 ) ) ) )
then A3: [#] Y0 c= [#] Y by PRE_TOPC:def 9;
thus the carrier of Y0 c= the carrier of Y by A1, A2, PRE_TOPC:def 9; :: 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 ) )
A4: ([#] Y0) \ ([#] Y) = {} by A3, 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 ) )
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 6;
then consider G being Subset of Y such that
A5: G is open and
A6: ([#] Y0) \ F0 = G /\ the carrier of Y0 by A2, Def1;
take F = ([#] Y) \ G; :: thesis: ( F is closed & F0 = F /\ the carrier of Y0 )
A7: G = ([#] Y) \ F by PRE_TOPC:22;
hence F is closed by A5, PRE_TOPC:def 6; :: thesis: F0 = F /\ the carrier of Y0
F0 = ([#] Y0) \ (G /\ the carrier of Y0) by A6, PRE_TOPC:22
.= (([#] Y0) \ G) \/ (([#] Y0) \ the carrier of Y0) by XBOOLE_1:54
.= (([#] Y0) \ G) \/ {} by XBOOLE_1:37
.= (([#] Y0) \ ([#] Y)) \/ (([#] Y0) /\ F) by A7, XBOOLE_1:52
.= ([#] Y0) /\ F by A4 ;
hence F0 = F /\ the carrier of Y0 ; :: thesis: verum

end;

given F being Subset of Y such that A8: F is closed and
A9: F0 = F /\ the carrier of Y0 ; :: thesis: F0 is closed
set G0 = ([#] Y0) \ F0;

now

take G = ([#] Y) \ F; :: thesis: ( G is open & ([#] Y0) \ F0 = G /\ the carrier of Y0 )
thus G is open by A8, PRE_TOPC:def 6; :: thesis: ([#] Y0) \ F0 = G /\ the carrier of Y0
A10: F = ([#] Y) \ G by PRE_TOPC:22;
([#] Y0) \ F0 = (([#] Y0) \ F) \/ (([#] Y0) \ the carrier of Y0) by A9, XBOOLE_1:54
.= (([#] Y0) \ F) \/ {} by XBOOLE_1:37
.= (([#] Y0) \ ([#] Y)) \/ (([#] Y0) /\ G) by A10, XBOOLE_1:52
.= ([#] Y0) /\ G by A4 ;
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 6; :: thesis: verum

end;

end;

assume A11: ( 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: Y0 is SubSpace of Y

now

thus the carrier of Y0 c= the carrier of Y by A11; :: 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 ) )
A12: ([#] Y0) \ ([#] Y) = {} by A11, XBOOLE_1:37;
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

set F0 = ([#] Y0) \ G0;
assume A13: G0 is open ; :: thesis: ex G being Subset of Y st
( G is open & G0 = G /\ the carrier of Y0 )
A14: G0 = ([#] Y0) \ (([#] Y0) \ G0) by PRE_TOPC:22;
then ([#] Y0) \ G0 is closed by A13, PRE_TOPC:def 6;
then consider F being Subset of Y such that
A15: F is closed and
A16: ([#] Y0) \ G0 = F /\ the carrier of Y0 by A11;
take G = ([#] Y) \ F; :: thesis: ( G is open & G0 = G /\ the carrier of Y0 )
A17: F = ([#] Y) \ G by PRE_TOPC:22;
thus G is open by A15, PRE_TOPC:def 6; :: thesis: G0 = G /\ the carrier of Y0
G0 = (([#] Y0) \ F) \/ (([#] Y0) \ the carrier of Y0) by A14, A16, XBOOLE_1:54
.= (([#] Y0) \ F) \/ {} by XBOOLE_1:37
.= (([#] Y0) \ ([#] Y)) \/ (([#] Y0) /\ G) by A17, 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 A18: G is open and
A19: G0 = G /\ the carrier of Y0 ; :: thesis: G0 is open
set F0 = ([#] Y0) \ G0;
A20: G0 = ([#] Y0) \ (([#] Y0) \ G0) by PRE_TOPC:22;

now

take F = ([#] Y) \ G; :: thesis: ( F is closed & ([#] Y0) \ G0 = F /\ the carrier of Y0 )
A21: G = ([#] Y) \ F by PRE_TOPC:22;
hence F is closed by A18, PRE_TOPC:def 6; :: thesis: ([#] Y0) \ G0 = F /\ the carrier of Y0
([#] Y0) \ G0 = (([#] Y0) \ G) \/ (([#] Y0) \ the carrier of Y0) by A19, XBOOLE_1:54
.= (([#] Y0) \ G) \/ {} by XBOOLE_1:37
.= (([#] Y0) \ ([#] Y)) \/ (([#] Y0) /\ F) by A21, XBOOLE_1:52
.= ([#] Y0) /\ F by A12 ;
hence ([#] Y0) \ G0 = F /\ the carrier of Y0 ; :: thesis: verum

end;

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

end;

end;

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