let X be set ; :: thesis: for c being Function of (bool X),(bool X) st c . {} = {} & ( for A being Subset of X holds A c= c . A ) & ( for A, B being Subset of X holds c . (A \/ B) = (c . A) \/ (c . B) ) & ( for A being Subset of X holds c . (c . A) = c . A ) holds

for T being TopStruct st the carrier of T = X & the topology of T = COMPLEMENT (rng c) holds

( T is TopSpace & ( for A being Subset of T holds Cl A = c . A ) )

let c be Function of (bool X),(bool X); :: thesis: ( c . {} = {} & ( for A being Subset of X holds A c= c . A ) & ( for A, B being Subset of X holds c . (A \/ B) = (c . A) \/ (c . B) ) & ( for A being Subset of X holds c . (c . A) = c . A ) implies for T being TopStruct st the carrier of T = X & the topology of T = COMPLEMENT (rng c) holds

( T is TopSpace & ( for A being Subset of T holds Cl A = c . A ) ) )

assume that

A1: c . {} = {} and

A2: for A being Subset of X holds A c= c . A and

A3: for A, B being Subset of X holds c . (A \/ B) = (c . A) \/ (c . B) and

A4: for A being Subset of X holds c . (c . A) = c . A ; :: thesis: for T being TopStruct st the carrier of T = X & the topology of T = COMPLEMENT (rng c) holds

( T is TopSpace & ( for A being Subset of T holds Cl A = c . A ) )

set F = rng c;

A5: dom c = bool X by FUNCT_2:def 1;

assume that

A19: the carrier of T = X and

A20: the topology of T = COMPLEMENT (rng c) ; :: thesis: ( T is TopSpace & ( for A being Subset of T holds Cl A = c . A ) )

{} = {} X ;

then A21: {} in rng c by A1, A5, FUNCT_1:def 3;

hence A22: T is TopSpace by A14, A19, A20, A6, Th4; :: thesis: for A being Subset of T holds Cl A = c . A

let A be Subset of T; :: thesis: Cl A = c . A

reconsider B = A, ClA = Cl A as Subset of X by A19;

reconsider cB = c . B as Subset of T by A19;

cB in rng c by A5, FUNCT_1:def 3;

then cB is closed by A19, A20, A21, A6, A14, Th4;

hence Cl A c= c . A by A2, TOPS_1:5; :: according to XBOOLE_0:def 10 :: thesis: c . A c= Cl A

ClA in rng c by A22, A19, A20, A21, A6, A14, Th4;

then ex a being object st

( a in dom c & ClA = c . a ) by FUNCT_1:def 3;

then c . ClA = ClA by A4;

hence c . A c= Cl A by A19, A13, PRE_TOPC:18; :: thesis: verum

for T being TopStruct st the carrier of T = X & the topology of T = COMPLEMENT (rng c) holds

( T is TopSpace & ( for A being Subset of T holds Cl A = c . A ) )

let c be Function of (bool X),(bool X); :: thesis: ( c . {} = {} & ( for A being Subset of X holds A c= c . A ) & ( for A, B being Subset of X holds c . (A \/ B) = (c . A) \/ (c . B) ) & ( for A being Subset of X holds c . (c . A) = c . A ) implies for T being TopStruct st the carrier of T = X & the topology of T = COMPLEMENT (rng c) holds

( T is TopSpace & ( for A being Subset of T holds Cl A = c . A ) ) )

assume that

A1: c . {} = {} and

A2: for A being Subset of X holds A c= c . A and

A3: for A, B being Subset of X holds c . (A \/ B) = (c . A) \/ (c . B) and

A4: for A being Subset of X holds c . (c . A) = c . A ; :: thesis: for T being TopStruct st the carrier of T = X & the topology of T = COMPLEMENT (rng c) holds

( T is TopSpace & ( for A being Subset of T holds Cl A = c . A ) )

set F = rng c;

A5: dom c = bool X by FUNCT_2:def 1;

A6: now :: thesis: for A, B being set st A in rng c & B in rng c holds

A \/ B in rng c

A \/ B in rng c

let A, B be set ; :: thesis: ( A in rng c & B in rng c implies A \/ B in rng c )

assume that

A7: A in rng c and

A8: B in rng c ; :: thesis: A \/ B in rng c

consider a being object such that

A9: a in dom c and

A10: A = c . a by A7, FUNCT_1:def 3;

consider b being object such that

A11: b in dom c and

A12: B = c . b by A8, FUNCT_1:def 3;

reconsider a = a, b = b as Subset of X by A9, A11;

A \/ B = (c . A) \/ B by A4, A9, A10

.= (c . A) \/ (c . B) by A4, A11, A12

.= c . ((c . a) \/ (c . b)) by A3, A10, A12 ;

hence A \/ B in rng c by A5, FUNCT_1:def 3; :: thesis: verum

end;assume that

A7: A in rng c and

A8: B in rng c ; :: thesis: A \/ B in rng c

consider a being object such that

A9: a in dom c and

A10: A = c . a by A7, FUNCT_1:def 3;

consider b being object such that

A11: b in dom c and

A12: B = c . b by A8, FUNCT_1:def 3;

reconsider a = a, b = b as Subset of X by A9, A11;

A \/ B = (c . A) \/ B by A4, A9, A10

.= (c . A) \/ (c . B) by A4, A11, A12

.= c . ((c . a) \/ (c . b)) by A3, A10, A12 ;

hence A \/ B in rng c by A5, FUNCT_1:def 3; :: thesis: verum

A13: now :: thesis: for A, B being Subset of X st A c= B holds

c . A c= c . B

c . A c= c . B

let A, B be Subset of X; :: thesis: ( A c= B implies c . A c= c . B )

assume A c= B ; :: thesis: c . A c= c . B

then A \/ B = B by XBOOLE_1:12;

then c . B = (c . A) \/ (c . B) by A3;

hence c . A c= c . B by XBOOLE_1:11; :: thesis: verum

end;assume A c= B ; :: thesis: c . A c= c . B

then A \/ B = B by XBOOLE_1:12;

then c . B = (c . A) \/ (c . B) by A3;

hence c . A c= c . B by XBOOLE_1:11; :: thesis: verum

A14: now :: thesis: for G being Subset-Family of X st G c= rng c holds

Intersect G in rng c

let T be TopStruct ; :: thesis: ( the carrier of T = X & the topology of T = COMPLEMENT (rng c) implies ( T is TopSpace & ( for A being Subset of T holds Cl A = c . A ) ) )Intersect G in rng c

let G be Subset-Family of X; :: thesis: ( G c= rng c implies Intersect G in rng c )

assume A15: G c= rng c ; :: thesis: Intersect G in rng c

Intersect G c= c . (Intersect G) by A2;

then c . (Intersect G) = Intersect G by A18;

hence Intersect G in rng c by A5, FUNCT_1:def 3; :: thesis: verum

end;assume A15: G c= rng c ; :: thesis: Intersect G in rng c

now :: thesis: for a being set st a in G holds

c . (Intersect G) c= a

then A18:
c . (Intersect G) c= Intersect G
by MSSUBFAM:4;c . (Intersect G) c= a

let a be set ; :: thesis: ( a in G implies c . (Intersect G) c= a )

assume A16: a in G ; :: thesis: c . (Intersect G) c= a

then reconsider A = a as Subset of X ;

A17: c . (Intersect G) c= c . A by A13, A16, MSSUBFAM:2;

ex b being object st

( b in dom c & A = c . b ) by A15, A16, FUNCT_1:def 3;

hence c . (Intersect G) c= a by A17, A4; :: thesis: verum

end;assume A16: a in G ; :: thesis: c . (Intersect G) c= a

then reconsider A = a as Subset of X ;

A17: c . (Intersect G) c= c . A by A13, A16, MSSUBFAM:2;

ex b being object st

( b in dom c & A = c . b ) by A15, A16, FUNCT_1:def 3;

hence c . (Intersect G) c= a by A17, A4; :: thesis: verum

Intersect G c= c . (Intersect G) by A2;

then c . (Intersect G) = Intersect G by A18;

hence Intersect G in rng c by A5, FUNCT_1:def 3; :: thesis: verum

assume that

A19: the carrier of T = X and

A20: the topology of T = COMPLEMENT (rng c) ; :: thesis: ( T is TopSpace & ( for A being Subset of T holds Cl A = c . A ) )

{} = {} X ;

then A21: {} in rng c by A1, A5, FUNCT_1:def 3;

hence A22: T is TopSpace by A14, A19, A20, A6, Th4; :: thesis: for A being Subset of T holds Cl A = c . A

let A be Subset of T; :: thesis: Cl A = c . A

reconsider B = A, ClA = Cl A as Subset of X by A19;

reconsider cB = c . B as Subset of T by A19;

cB in rng c by A5, FUNCT_1:def 3;

then cB is closed by A19, A20, A21, A6, A14, Th4;

hence Cl A c= c . A by A2, TOPS_1:5; :: according to XBOOLE_0:def 10 :: thesis: c . A c= Cl A

ClA in rng c by A22, A19, A20, A21, A6, A14, Th4;

then ex a being object st

( a in dom c & ClA = c . a ) by FUNCT_1:def 3;

then c . ClA = ClA by A4;

hence c . A c= Cl A by A19, A13, PRE_TOPC:18; :: thesis: verum