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 ; :: 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 ;
hence f . x in A by FUNCT_1:def 7; :: thesis: verum
end;
then A12: f . x in meet F by ;
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 ; :: 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 ;
hence B is closed by ; :: 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 ;
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 ;
hence x in B by ; :: thesis: verum
end;
hence x in meet F1 by ; :: thesis: verum
end;
then meet F1 = f " (meet F) by A9;
hence meet F is closed by ; :: 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