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;

A6: now :: thesis: for A, B being set st A in rng c & B in rng c holds
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;

A13: now :: thesis: for A, B being Subset of X st A c= B holds
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;

A14: now :: thesis: for G being Subset-Family of X st G c= rng c holds
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

now :: thesis: for a being set st a in G holds
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;

then A18: c . (Intersect G) c= Intersect G by MSSUBFAM:4;
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;

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