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

set F = rng c;

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 that

A5: the carrier of T = X and

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

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

hence A21: T is TopSpace by A16, A5, A6, 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;

IntA in rng c by A21, A6, PRE_TOPC:def 2;

then ex a being object st

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

then c . IntA = IntA by A4;

hence Int A c= c . A by A5, A15, TOPS_1:16; :: according to XBOOLE_0:def 10 :: thesis: c . A c= Int A

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

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

then cB is open by A6;

hence c . A c= Int A by A2, TOPS_1:24; :: thesis: verum

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

set F = rng c;

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 that

A5: the carrier of T = X and

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

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

A8: now :: thesis: for A, B being Subset of T st A in rng c & B in rng c holds

A /\ B in rng c

A /\ B in rng c

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

assume that

A9: A in rng c and

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

consider a being object such that

A11: a in dom c and

A12: A = c . a by A9, FUNCT_1:def 3;

consider b being object such that

A13: b in dom c and

A14: B = c . b by A10, FUNCT_1:def 3;

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

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

.= (c . A) /\ (c . B) by A4, A13, A14

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

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

end;assume that

A9: A in rng c and

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

consider a being object such that

A11: a in dom c and

A12: A = c . a by A9, FUNCT_1:def 3;

consider b being object such that

A13: b in dom c and

A14: B = c . b by A10, FUNCT_1:def 3;

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

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

.= (c . A) /\ (c . B) by A4, A13, A14

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

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

A15: 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 = 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;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

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

union G in rng c

X in rng c
by A1, A7, FUNCT_1:def 3;union G in rng c

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

assume A17: G c= rng c ; :: thesis: union G in rng c

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

then c . (union G) = union G by A20;

hence union G in rng c by A7, FUNCT_1:def 3; :: thesis: verum

end;assume A17: G c= rng c ; :: thesis: union G in rng c

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

a c= c . (union G)

then A20:
union G c= c . (union G)
by ZFMISC_1:76;a c= c . (union G)

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

assume A18: a in G ; :: thesis: a c= c . (union G)

then reconsider A = a as Subset of X ;

A19: c . A c= c . (union G) by A15, A18, ZFMISC_1:74;

ex b being object st

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

hence a c= c . (union G) by A19, A4; :: thesis: verum

end;assume A18: a in G ; :: thesis: a c= c . (union G)

then reconsider A = a as Subset of X ;

A19: c . A c= c . (union G) by A15, A18, ZFMISC_1:74;

ex b being object st

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

hence a c= c . (union G) by A19, A4; :: thesis: verum

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

then c . (union G) = union G by A20;

hence union G in rng c by A7, FUNCT_1:def 3; :: thesis: verum

hence A21: T is TopSpace by A16, A5, A6, 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;

IntA in rng c by A21, A6, PRE_TOPC:def 2;

then ex a being object st

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

then c . IntA = IntA by A4;

hence Int A c= c . A by A5, A15, TOPS_1:16; :: according to XBOOLE_0:def 10 :: thesis: c . A c= Int A

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

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

then cB is open by A6;

hence c . A c= Int A by A2, TOPS_1:24; :: thesis: verum