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

then A3: {} S is closed by A1;

A4: for F being Subset-Family of S st F is closed holds

meet F is closed

then [#] S is closed by A1;

hence S is TopSpace by A3, A2, A4, Th5; :: thesis: verum

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

( {} T is closed & f " {} = {} )
;
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;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

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

f " ([#] S) = [#] T
by TOPS_2:41;
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

end;assume A5: F is closed ; :: thesis: meet F is closed

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

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

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

A9: meet F1 c= f " (meet F)

f " (meet F) c= meet F1

hence meet F is closed by A1, A15; :: thesis: verum

end;ex A being set st A in F

proof

then consider A being Subset of S such that
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;take the Element of F ; :: thesis: the Element of F in F

thus the Element of F in F by A6; :: thesis: verum

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

then reconsider F1 = { (f " A) where A is Subset of S : A in F } as Subset-Family of T ;
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;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

A9: meet F1 c= f " (meet F)

proof

F1 is closed
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

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

then A12:
f . x in meet F
by A6, SETFAM_1:def 1;
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;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

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

proof

then A15:
meet F1 is closed
by TOPS_2:22;
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;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

f " (meet F) c= meet F1

proof

then
meet F1 = f " (meet F)
by A9;
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

end;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

hence
x in meet F1
by A8, SETFAM_1:def 1; :: thesis: verum
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;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

hence meet F is closed by A1, A15; :: thesis: verum

then [#] S is closed by A1;

hence S is TopSpace by A3, A2, A4, Th5; :: thesis: verum