let X be set ; 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); ( 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
; 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 ; ( 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
; ( 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 for A, B being Subset of T st A in rng c & B in rng c holds
A /\ B in rng clet A,
B be
Subset of
T;
( 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
;
A /\ B in rng cconsider 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;
verum end;
X in rng c
by A1, A7, FUNCT_1:def 3;
hence A21:
T is TopSpace
by A16, A5, A6, A8, PRE_TOPC:def 1; for A being Subset of T holds Int A = c . A
let A be Subset of T; 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; XBOOLE_0:def 10 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; verum