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;
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
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;
A15: 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 = 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;
A16: now :: thesis: for G being Subset-Family of X st G c= rng c holds
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
now :: thesis: for a being set st a in G holds
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;
then A20: union G c= c . (union G) by ZFMISC_1:76;
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;
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; :: 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