let X be set ; :: thesis: for i being Function of bool X, bool X st i . X = X & ( for A being Subset of X holds i . A c= A ) & ( for A, B being Subset of X holds i . (A /\ B) = (i . A) /\ (i . B) ) & ( for A being Subset of X holds i . (i . A) = i . A ) holds
for T being TopStruct st the carrier of T = X & the topology of T = rng i holds
( T is TopSpace & ( for A being Subset of T holds Int A = i . A ) )
let c be Function of bool X, bool X; :: thesis: ( c . X = X & ( for A being Subset of X holds c . A 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 = rng c holds
( T is TopSpace & ( for A being Subset of T holds Int A = c . A ) ) )
assume that
A1: c . X = X and
A2: for A being Subset of X holds c . A 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 = rng c holds
( T is TopSpace & ( for A being Subset of T holds Int A = c . A ) )
let T be TopStruct ; :: thesis: ( the carrier of T = X & the topology of T = rng c implies ( T is TopSpace & ( for A being Subset of T holds Int A = c . A ) ) )
assume A5: ( the carrier of T = X & the topology of T = rng c ) ; :: thesis: ( T is TopSpace & ( for A being Subset of T holds Int A = c . A ) )
A6: dom c = bool X by FUNCT_2:def 1;
set F = rng c;
( X = [#] X & {} = {} X ) ;
then A7: X in rng c by A1, A6, FUNCT_1:def 5;

A8: now

let A, B be Subset of T; :: thesis: ( A in rng c & B in rng c implies A /\ B in rng c )
assume A9: ( A in rng c & B in rng c ) ; :: thesis: A /\ B in rng c
then consider a being set such that
A10: ( a in dom c & A = c . a ) by FUNCT_1:def 5;
consider b being set such that
A11: ( b in dom c & B = c . b ) by A9, FUNCT_1:def 5;
reconsider a = a, b = b as Subset of X by A10, A11;
A /\ B = (c . A) /\ B by A4, A10
.= (c . A) /\ (c . B) by A4, A11
.= c . ((c . a) /\ (c . b)) by A3, A10, A11 ;
hence A /\ B in rng c by A6, FUNCT_1:def 5; :: thesis: verum

end;

A12: now

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 = A by XBOOLE_1:28;
then c . A = (c . A) /\ (c . B) by A3;
hence c . A c= c . B by XBOOLE_1:17; :: thesis: verum

end;

now

let G be Subset-Family of X; :: thesis: ( G c= rng c implies union G in rng c )
assume A13: G c= rng c ; :: thesis: union G in rng c
A14: c . (union G) c= union G by A2;

now

let a be set ; :: thesis: ( a in G implies a c= c . (union G) )
assume A15: a in G ; :: thesis: a c= c . (union G)
then reconsider A = a as Subset of X ;
A16: ex b being set st
( b in dom c & A = c . b ) by A13, A15, FUNCT_1:def 5;
c . A c= c . (union G) by A12, A15, ZFMISC_1:92;
hence a c= c . (union G) by A4, A16; :: thesis: verum

end;

then union G c= c . (union G) by ZFMISC_1:94;
then c . (union G) = union G by A14, XBOOLE_0:def 10;
hence union G in rng c by A6, FUNCT_1:def 5; :: thesis: verum

end;

hence A17: T is TopSpace by A5, A7, A8, PRE_TOPC:def 1; :: thesis: for A being Subset of T holds Int A = c . A
let A be Subset of T; :: thesis: Int A = c . A
reconsider B = A, IntA = Int A as Subset of X by A5;
reconsider cB = c . B as Subset of T by A5;
Int A is open by A17;
then IntA in rng c by A5, PRE_TOPC:def 5;
then ex a being set st
( a in dom c & IntA = c . a ) by FUNCT_1:def 5;
then ( c . IntA = IntA & Int A c= A ) by A4, TOPS_1:44;
hence Int A c= c . A by A5, A12; :: according to XBOOLE_0:def 10 :: thesis: c . A c= Int A
cB in rng c by A6, FUNCT_1:def 5;
then ( cB is open & c . B c= B ) by A2, A5, PRE_TOPC:def 5;
hence c . A c= Int A by TOPS_1:56; :: thesis: verum