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: {} S is closed

proof

A3: {} T is closed ;
f " {} = {} by RELAT_1:171;
hence {} S is closed by A1, A3; :: thesis: verum

end;

A4: [#] S is closed

proof

f " ([#] S) = [#] T by TOPS_2:52;
hence [#] S is closed by A1; :: thesis: verum

end;

A5: 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:36;
then f " (A \/ B) is closed by RELAT_1:175;
hence A \/ B is closed by A1; :: thesis: verum

end;

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 A6: 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 A2, SETFAM_1:def 1; :: thesis: verum

end;

suppose A7: 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

consider A being Element of F;
take A ; :: thesis: A in F
thus A in F by A7; :: thesis: verum

end;

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

proof

let B be set ; :: 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 consider A being Subset of S such that
A10: ( B = f " A & A in F ) ;
thus B in bool the carrier of T by A10; :: thesis: verum

end;

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

proof

thus meet F1 c= f " (meet F) :: according to XBOOLE_0:def 10 :: thesis: f " (meet F) c= meet F1

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in meet F1 or x in f " (meet F) )
assume A12: x in meet F1 ; :: thesis: x in f " (meet F)
then x in the carrier of T ;
then A13: x in dom f by FUNCT_2:def 1;
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 A14: A in F ; :: thesis: f . x in A
then reconsider A = A as Subset of S ;
f " A in F1 by A14;
then x in f " A by A12, SETFAM_1:def 1;
hence f . x in A by FUNCT_1:def 13; :: thesis: verum

end;

then f . x in meet F by A7, SETFAM_1:def 1;
hence x in f " (meet F) by A13, FUNCT_1:def 13; :: thesis: verum

end;

thus f " (meet F) c= meet F1 :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in f " (meet F) or x in meet F1 )
assume x in f " (meet F) ; :: thesis: x in meet F1
then A15: ( x in dom f & f . x in meet F ) by FUNCT_1:def 13;
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
A16: ( B = f " A & A in F ) ;
f . x in A by A15, A16, SETFAM_1:def 1;
hence x in B by A15, A16, FUNCT_1:def 13; :: thesis: verum

end;

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

end;

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
A17: ( f " A = B & A in F ) ;
A is closed by A6, A17, TOPS_2:def 2;
hence B is closed by A1, A17; :: thesis: verum

end;

then meet F1 is closed by TOPS_2:29;
hence meet F is closed by A1, A11; :: thesis: verum

end;

end;

end;

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