let T be TopSpace; :: thesis: for S being non empty TopStruct
for f being Function of T,S st ( for A being Subset of S holds
( A is closed iff f " A is closed ) ) holds
S is TopSpace
let S be non empty TopStruct ; :: thesis: for f being Function of T,S st ( for A being Subset of S holds
( A is closed iff f " A is closed ) ) holds
S is TopSpace
let f be Function of T,S; :: thesis: ( ( for A being Subset of S holds
( A is closed iff f " A is closed ) ) implies S is TopSpace )
assume A1: for A being Subset of S holds
( A is closed iff f " A is closed ) ; :: thesis: S is TopSpace
A2: for A, B being Subset of S st A is closed & B is closed holds
A \/ B is closed

proof

let A, B be Subset of S; :: thesis: ( A is closed & B is closed implies A \/ B is closed )
assume ( A is closed & B is closed ) ; :: thesis: A \/ B is closed
then ( f " A is closed & f " B is closed ) by A1;
then (f " A) \/ (f " B) is closed by TOPS_1:9;
then f " (A \/ B) is closed by RELAT_1:140;
hence A \/ B is closed by A1; :: thesis: verum

end;

( {} T is closed & f " {} = {} ) ;
then A3: {} S is closed by A1;
A4: for F being Subset-Family of S st F is closed holds
meet F is closed

proof

let F be Subset-Family of S; :: thesis: ( F is closed implies meet F is closed )
assume A5: F is closed ; :: thesis: meet F is closed

per cases ( F = {} S or F <> {} ) ;

suppose F = {} S ; :: thesis: meet F is closed

hence meet F is closed by A3, SETFAM_1:def 1; :: thesis: verum

end;

suppose A6: F <> {} ; :: thesis: meet F is closed

set F1 = { (f " A) where A is Subset of S : A in F } ;
ex A being set st A in F

proof

set A = the Element of F;
take the Element of F ; :: thesis: the Element of F in F
thus the Element of F in F by A6; :: thesis: verum

end;

then consider A being Subset of S such that
A7: A in F ;
reconsider A = A as Subset of S ;
A8: f " A in { (f " A) where A is Subset of S : A in F } by A7;
{ (f " A) where A is Subset of S : A in F } c= bool the carrier of T

proof

let B be object ; :: according to TARSKI:def 3 :: thesis: ( not B in { (f " A) where A is Subset of S : A in F } or B in bool the carrier of T )
assume B in { (f " A) where A is Subset of S : A in F } ; :: thesis: B in bool the carrier of T
then ex A being Subset of S st
( B = f " A & A in F ) ;
hence B in bool the carrier of T ; :: thesis: verum

end;

then reconsider F1 = { (f " A) where A is Subset of S : A in F } as Subset-Family of T ;
A9: meet F1 c= f " (meet F)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in meet F1 or x in f " (meet F) )
assume A10: x in meet F1 ; :: thesis: x in f " (meet F)
for A being set st A in F holds
f . x in A

proof

let A be set ; :: thesis: ( A in F implies f . x in A )
assume A11: A in F ; :: thesis: f . x in A
then reconsider A = A as Subset of S ;
f " A in F1 by A11;
then x in f " A by A10, SETFAM_1:def 1;
hence f . x in A by FUNCT_1:def 7; :: thesis: verum

end;

then A12: f . x in meet F by A6, SETFAM_1:def 1;
x in the carrier of T by A10;
then x in dom f by FUNCT_2:def 1;
hence x in f " (meet F) by A12, FUNCT_1:def 7; :: thesis: verum

end;

F1 is closed

proof

let B be Subset of T; :: according to TOPS_2:def 2 :: thesis: ( not B in F1 or B is closed )
assume B in F1 ; :: thesis: B is closed
then consider A being Subset of S such that
A13: f " A = B and
A14: A in F ;
A is closed by A5, A14;
hence B is closed by A1, A13; :: thesis: verum

end;

then A15: meet F1 is closed by TOPS_2:22;
f " (meet F) c= meet F1

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in f " (meet F) or x in meet F1 )
assume A16: x in f " (meet F) ; :: thesis: x in meet F1
then A17: f . x in meet F by FUNCT_1:def 7;
A18: x in dom f by A16, FUNCT_1:def 7;
for B being set st B in F1 holds
x in B

proof

let B be set ; :: thesis: ( B in F1 implies x in B )
assume B in F1 ; :: thesis: x in B
then consider A being Subset of S such that
A19: B = f " A and
A20: A in F ;
f . x in A by A17, A20, SETFAM_1:def 1;
hence x in B by A18, A19, FUNCT_1:def 7; :: thesis: verum

end;

hence x in meet F1 by A8, SETFAM_1:def 1; :: thesis: verum

end;

then meet F1 = f " (meet F) by A9;
hence meet F is closed by A1, A15; :: thesis: verum

end;

end;

end;

f " ([#] S) = [#] T by TOPS_2:41;
then [#] S is closed by A1;
hence S is TopSpace by A3, A2, A4, Th5; :: thesis: verum