Copyright (c) 1989 Association of Mizar Users
environ
vocabulary PRE_TOPC, SETFAM_1, SUBSET_1, BOOLE, TARSKI, FINSET_1, FUNCT_1,
RELAT_1, FINSEQ_1, ORDINAL2, TOPS_2, SEQ_1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XREAL_0, RELAT_1, FUNCT_1,
FUNCT_2, FUNCT_3, NAT_1, FINSEQ_1, FINSET_1, SETFAM_1, STRUCT_0,
PRE_TOPC;
constructors FUNCT_3, NAT_1, FINSEQ_1, PRE_TOPC, XREAL_0, MEMBERED;
clusters PRE_TOPC, STRUCT_0, RELSET_1, ARYTM_3, MEMBERED, ZFMISC_1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, PRE_TOPC;
theorems TARSKI, FINSET_1, SETFAM_1, FUNCT_1, FUNCT_2, FUNCT_3, NAT_1,
FINSEQ_1, ZFMISC_1, PRE_TOPC, TOPS_1, RELAT_1, REAL_1, RELSET_1,
XBOOLE_0, XBOOLE_1, SUBSET_1;
schemes FUNCT_1, NAT_1, PRE_TOPC;
begin
reserve x, y for set,
k for Nat,
T for TopStruct,
GX for TopSpace,
P, Q for Subset of T,
M, N for Subset of T,
F, G for Subset-Family of T,
W, Z for Subset-Family of GX,
A for SubSpace of T;
::
:: A FAMILY OF SETS IN TOPOLOGICAL SPACES
::
theorem Th1:
for T being 1-sorted,
F being Subset-Family of T holds
F c= bool [#]T
proof
let T be 1-sorted,
F be Subset-Family of T;
F c= bool the carrier of T;
hence F c= bool [#]T by PRE_TOPC:12;
end;
canceled;
theorem Th3:
for T being 1-sorted,
F being Subset-Family of T,
X being set st X c= F holds X is Subset-Family of T
proof
let T be 1-sorted,
F be Subset-Family of T,
X be set;
assume A1: X c= F;
X c= bool the carrier of T
proof
let y;
assume y in X;
then y in F by A1;
hence y in bool the carrier of T;
end;
then X is Subset-Family of T by SETFAM_1:def 7;
hence thesis;
end;
canceled;
theorem
for T being non empty 1-sorted, F being Subset-Family of T st
F is_a_cover_of T holds F <> {}
proof let T be non empty 1-sorted, F be Subset-Family of T;
assume F is_a_cover_of T;
then A1: union F = [#]T by PRE_TOPC:def 8
.= the carrier of T by PRE_TOPC:12;
consider x being Element of union F;
ex A being set st x in A & A in F by A1,TARSKI:def 4;
hence thesis;
end;
theorem
for T being 1-sorted, F, G being Subset-Family of T holds
union F \ union G c= union(F \ G)
proof
let T be 1-sorted, F, G be Subset-Family of T;
let x; assume x in union F \ union G;
then A1: x in union F & not x in union G by XBOOLE_0:def 4;
then consider A being set such that A2: x in A & A in F by TARSKI:def 4;
not A in G by A1,A2,TARSKI:def 4;
then x in A & A in F \ G by A2,XBOOLE_0:def 4;
hence thesis by TARSKI:def 4;
end;
canceled 2;
theorem
for T being 1-sorted, F being Subset-Family of T holds
COMPLEMENT(COMPLEMENT(F)) = F;
theorem
for T being 1-sorted, F being Subset-Family of T holds
F <> {} iff COMPLEMENT(F) <> {}
proof
let T be 1-sorted, F be Subset-Family of T;
thus F <> {} implies COMPLEMENT(F) <> {} by SETFAM_1:46;
assume COMPLEMENT(F) <> {};
then COMPLEMENT(COMPLEMENT(F)) <> {} by SETFAM_1:46;
hence thesis;
end;
theorem Th11:
for T being 1-sorted, F being Subset-Family of T holds
F <> {} implies meet COMPLEMENT(F) = (union F)`
proof
let T be 1-sorted, F be Subset-Family of T;
assume F <> {};
then meet COMPLEMENT(F) = [#](the carrier of T) \ union F by SETFAM_1:47;
then meet COMPLEMENT(F) = (the carrier of T) \ union F by SUBSET_1:def 4;
then meet COMPLEMENT(F) = [#]T \ union F by PRE_TOPC:def 3;
hence thesis by PRE_TOPC:17;
end;
theorem Th12:
for T being 1-sorted, F being Subset-Family of T holds
F <> {} implies union COMPLEMENT(F) = (meet F)`
proof
let T be 1-sorted, F be Subset-Family of T;
assume F <> {};
then union COMPLEMENT(F) = [#](the carrier of T) \ meet F by SETFAM_1:48
.= (the carrier of T) \ meet F by SUBSET_1:def 4;
then union COMPLEMENT(F) = [#]T \ meet F by PRE_TOPC:def 3;
hence thesis by PRE_TOPC:17;
end;
theorem Th13:
for T being 1-sorted, F being Subset-Family of T holds
COMPLEMENT(F) is finite iff F is finite
proof
let T be 1-sorted, F be Subset-Family of T;
thus COMPLEMENT(F) is finite implies F is finite
proof
assume A1: COMPLEMENT(F) is finite;
defpred X[set,set] means
for X being Subset of T st X = $1 holds $2 = X`;
A2: for x,y1,y2 being set st x in COMPLEMENT(F) & X[x,y1] & X[x,y2]
holds y1 = y2
proof
let x,y1,y2 be set such that A3: x in COMPLEMENT(F) and
A4: for X being Subset of T st X = x holds y1 = X` and
A5: for X being Subset of T st X = x holds y2 = X`;
reconsider X=x as Subset of T by A3;
y1 = X` by A4;
hence thesis by A5;
end;
A6: for x st x in COMPLEMENT(F) ex y st X[x,y]
proof
let x; assume x in COMPLEMENT(F);
then reconsider X=x as Subset of T;
reconsider y=X` as set;
take y;
thus thesis;
end;
consider f being Function such that A7: dom f = COMPLEMENT(F) and
A8: for x st x in COMPLEMENT(F) holds X[x,f.x] from FuncEx(A2,A6);
x in rng f iff x in F
proof
hereby assume x in rng f;
then consider y such that A9: y in dom f and A10: x=f.y by FUNCT_1:def
5;
reconsider Y=y as Subset of T by A7,A9;
Y` in F by A7,A9,SETFAM_1:def 8;
hence x in F by A7,A8,A9,A10;
end;
assume A11: x in F;
then reconsider X=x as Subset of T;
A12: X`` = X;
then A13: X` in COMPLEMENT(F) by A11,SETFAM_1:def 8;
A14: X` in dom f by A7,A11,A12,SETFAM_1:def 8;
f.(X`) = X`` by A8,A13;
hence x in rng f by A14,FUNCT_1:def 5;
end;
then rng f = F by TARSKI:2;
then f.:(COMPLEMENT(F)) = F by A7,RELAT_1:146;
hence thesis by A1,FINSET_1:17;
end;
thus F is finite implies COMPLEMENT(F) is finite
proof
assume A15: F is finite;
defpred X[set,set] means
for X being Subset of T st X = $1 holds $2 = X`;
A16: for x,y1,y2 being set st x in F & X[x,y1] & X[x,y2]
holds y1 = y2
proof
let x,y1,y2 be set such that A17: x in F and
A18: for X being Subset of T st X = x holds y1 = X` and
A19: for X being Subset of T st X = x holds y2 = X`;
reconsider X=x as Subset of T by A17;
y1 = X` by A18;
hence thesis by A19;
end;
A20: for x st x in F ex y st X[x,y]
proof
let x; assume x in F;
then reconsider X=x as Subset of T;
reconsider y=X` as set;
take y;
thus thesis;
end;
consider f being Function such that A21: dom f = F and
A22: for x st x in F holds X[x,f.x] from FuncEx(A16,A20);
x in rng f iff x in COMPLEMENT(F)
proof
hereby assume x in rng f;
then consider y such that A23: y in
dom f and A24: x=f.y by FUNCT_1:def 5;
reconsider Y=y as Subset of T by A21,A23;
Y in F & Y``=Y by A21,A23;
then Y` in COMPLEMENT(F) by SETFAM_1:def 8;
hence x in COMPLEMENT(F) by A21,A22,A23,A24;
end;
assume A25: x in COMPLEMENT(F);
then reconsider X=x as Subset of T;
A26: X` in F by A25,SETFAM_1:def 8;
A27: X` in dom f by A21,A25,SETFAM_1:def 8;
f.(X` qua set) = X`` by A22,A26;
hence x in rng f by A27,FUNCT_1:def 5;
end;
then rng f = COMPLEMENT(F) by TARSKI:2;
then f.:(F) = COMPLEMENT(F) by A21,RELAT_1:146;
hence thesis by A15,FINSET_1:17;
end;
end;
::
:: CLOSED AND OPEN FAMILIES
::
definition let T be TopStruct, F be Subset-Family of T;
attr F is open means
:Def1: for P being Subset of T holds P in F implies P is open;
attr F is closed means
:Def2: for P being Subset of T holds P in F implies P is closed;
end;
canceled 2;
theorem Th16:
F is closed iff COMPLEMENT(F) is open
proof
thus F is closed implies COMPLEMENT(F) is open
proof
assume A1: F is closed;
let P; assume P in COMPLEMENT(F);
then P` in F by SETFAM_1:def 8;
then P` in F;
then P` is closed by A1,Def2;
hence thesis by TOPS_1:30;
end;
assume A2: COMPLEMENT(F) is open;
let P such that A3: P in F;
P``=P;
then P` in COMPLEMENT(F) by A3,SETFAM_1:def 8;
then P` in COMPLEMENT(F);
then P` is open by A2,Def1;
hence thesis by TOPS_1:29;
end;
theorem
F is open iff COMPLEMENT(F) is closed
proof
thus F is open implies COMPLEMENT(F) is closed
proof
assume A1: F is open;
let P; assume P in COMPLEMENT(F);
then P` in F by SETFAM_1:def 8;
then P` in F;
then P` is open by A1,Def1;
hence thesis by TOPS_1:29;
end;
assume A2: COMPLEMENT(F) is closed;
let P such that A3: P in F;
P``=P;
then P` in COMPLEMENT(F) by A3,SETFAM_1:def 8;
then P` in COMPLEMENT(F);
then P` is closed by A2,Def2;
hence thesis by TOPS_1:30;
end;
theorem
F c= G & G is open implies F is open
proof
assume that A1: F c= G and A2:G is open;
let P; assume P in F;
hence thesis by A1,A2,Def1;
end;
theorem
F c= G & G is closed implies F is closed
proof
assume that A1: F c= G and A2:G is closed;
let P; assume P in F;
hence thesis by A1,A2,Def2;
end;
theorem
F is open & G is open implies F \/ G is open
proof
assume that A1: F is open and A2: G is open;
let P; assume P in F \/ G;
then P in F or P in G by XBOOLE_0:def 2;
hence P is open by A1,A2,Def1;
end;
theorem
F is open implies F /\ G is open
proof
assume A1: F is open;
let P; assume P in F /\ G;
then P in F by XBOOLE_0:def 3;
hence P is open by A1,Def1;
end;
theorem
F is open implies F \ G is open
proof
assume A1: F is open;
let P; assume P in F \ G;
then P in F by XBOOLE_0:def 4;
hence P is open by A1,Def1;
end;
theorem
F is closed & G is closed implies F \/ G is closed
proof
assume that A1: F is closed and A2: G is closed;
let P; assume P in F \/ G;
then P in F or P in G by XBOOLE_0:def 2;
hence P is closed by A1,A2,Def2;
end;
theorem
F is closed implies F /\ G is closed
proof
assume A1: F is closed;
let P; assume P in F /\ G;
then P in F by XBOOLE_0:def 3;
hence P is closed by A1,Def2;
end;
theorem
F is closed implies F \ G is closed
proof
assume A1: F is closed;
let P; assume P in F \ G;
then P in F by XBOOLE_0:def 4;
hence P is closed by A1,Def2;
end;
theorem Th26:
W is open implies union W is open
proof
assume A1: W is open;
W c= the topology of GX
proof
let x; assume A2: x in W;
then reconsider X=x as Subset of GX;
X is open by A1,A2,Def1;
hence thesis by PRE_TOPC:def 5;
end;
then union W in the topology of GX by PRE_TOPC:def 1;
hence thesis by PRE_TOPC:def 5;
end;
theorem Th27:
W is open & W is finite implies meet W is open
proof
assume that A1: W is open and A2: W is finite;
consider p being FinSequence such that A3: rng p = W by A2,FINSEQ_1:73;
consider n being Nat such that A4: dom p = Seg n by FINSEQ_1:def 2;
defpred X[Nat] means
for Z st Z = p.:(Seg $1) & $1 <= n & 1 <= n holds meet Z is open;
A5: X[0]
proof
let Z; assume that A6: Z = p.:(Seg 0) and 0 <= n;
A7: meet Z = {} by A6,FINSEQ_1:4,RELAT_1:149,SETFAM_1:2;
{} in the topology of GX by PRE_TOPC:5;
hence thesis by A7,PRE_TOPC:def 5;
end;
A8: X[k] implies X[k+1]
proof
assume A9: for Z st Z = p.:(Seg k) & k <= n & 1 <= n holds meet Z is open;
let Z such that A10: Z = p.:(Seg(k+1)); assume A11: k+1 <= n & 1 <= n;
A12: now assume k=0;
then A13: Seg(k+1) = {1} & 1 in dom p by A4,A11,FINSEQ_1:3,4;
then p.:Seg(k+1) = {p.1} by FUNCT_1:117;
then meet Z = p.1 by A10,SETFAM_1:11;
then meet Z in W by A3,A13,FUNCT_1:def 5;
hence meet Z is open by A1,Def1;
end;
now assume A14: 0 < k;
0+1 = 1;
then 1 <= 1 & 1 <= k by A14,NAT_1:38;
then A15: Seg k <> {} by FINSEQ_1:3;
k+1 <= n+1 by A11,NAT_1:37;
then k <= n by REAL_1:53;
then A16: Seg k c= dom p by A4,FINSEQ_1:7;
A17: p.:(Seg(k+1)) = p.:(Seg k \/ {k+1}) by FINSEQ_1:11
.= p.:(Seg k) \/ p.:{k+1} by RELAT_1:153;
p.:(Seg k) c= W by A3,RELAT_1:144;
then reconsider G1 = p.:(Seg k) as Subset-Family of GX by Th3;
A18: G1 <> {} by A15,A16,RELAT_1:152;
p.:{k+1} c= W by A3,RELAT_1:144;
then reconsider G2 = p.:{k+1} as Subset-Family of GX by Th3;
0 <= k & 0+1 = 1 by NAT_1:18;
then 1 <= k+1 & k+1 <= n by A11,REAL_1:55;
then A19: k+1 in dom p by A4,FINSEQ_1:3;
then {k+1} <> {} & {k+1} c= dom p by ZFMISC_1:37;
then G2 <> {} by RELAT_1:152;
then A20: meet Z = meet G1 /\ meet G2 by A10,A17,A18,SETFAM_1:10;
G2 = {p.(k+1)} by A19,FUNCT_1:117;
then A21: meet G2 = p.(k+1) & p.(k+1) in
W by A3,A19,FUNCT_1:def 5,SETFAM_1:11
;
k+1 <= n+1 by A11,NAT_1:37;
then k <= n by REAL_1:53;
then meet G1 is open & meet G2 is open by A1,A9,A11,A21,Def1;
hence meet Z is open by A20,TOPS_1:38;
end;
hence thesis by A12,NAT_1:19;
end;
A22: X[k] from Ind(A5,A8);
A23: now assume
A24: 1 <= n;
W = p.:(Seg n) by A3,A4,RELAT_1:146;
hence meet W is open by A22,A24;
end;
A25:now assume n = 0;
then W = p.:{} by A3,A4,FINSEQ_1:4,RELAT_1:146;
then A26: meet W = {} by RELAT_1:149,SETFAM_1:2;
{} in the topology of GX by PRE_TOPC:5;
hence meet W is open by A26,PRE_TOPC:def 5;
end;
now assume n <> 0;
then 0 < n & 1 = 0+1 by NAT_1:19;
hence 1 <= n by NAT_1:38;
end;
hence thesis by A23,A25;
end;
theorem
W is closed & W is finite implies union W is closed
proof
assume that A1: W is closed and A2: W is finite;
reconsider C = COMPLEMENT(W) as Subset-Family of GX;
COMPLEMENT(W) is open & COMPLEMENT(W) is finite by A1,A2,Th13,Th16;
then A3: meet C is open by Th27;
A4: now assume W <> {};
then meet COMPLEMENT(W) = (union W)` by Th11;
hence union W is closed by A3,TOPS_1:29;
end;
now assume W = {};
then union W = {}GX by ZFMISC_1:2;
hence union W is closed by TOPS_1:22;
end;
hence thesis by A4;
end;
theorem
W is closed implies meet W is closed
proof
reconsider C = COMPLEMENT(W) as Subset-Family of GX;
assume W is closed;
then COMPLEMENT(W) is open by Th16;
then A1: union C is open by Th26;
A2: now assume W <> {};
then union COMPLEMENT(W) = (meet W)` by Th12;
hence meet W is closed by A1,TOPS_1:29;
end;
now assume W = {};
then meet W = {}GX by SETFAM_1:def 1;
hence meet W is closed by TOPS_1:22;
end;
hence thesis by A2;
end;
::
:: SUBSPACES OF A TOPOLOGICAL SPACE
::
canceled;
theorem
for F being Subset-Family of A holds
F is Subset-Family of T
proof
let F be Subset-Family of A;
[#] A c= [#]T by PRE_TOPC:def 9;
then [#] A c= the carrier of T by PRE_TOPC:12;
then the carrier of A c= the carrier of T by PRE_TOPC:12;
then bool the carrier of A c= bool the carrier of T by ZFMISC_1:79;
then F c= bool the carrier of T by XBOOLE_1:1;
then F is Subset-Family of T by SETFAM_1:def 7;
hence thesis;
end;
theorem Th32:
for B being Subset of A holds B is open
iff ex C being Subset of T st C is open & C /\ [#](A) = B
proof
let B be Subset of A;
hereby assume B is open;
then B in the topology of A by PRE_TOPC:def 5;
then consider C being Subset of T such that
A1: C in the topology of T & C /\ [#](A) = B by PRE_TOPC:def 9;
reconsider C as Subset of T;
take C;
thus C is open & C /\ [#] A = B by A1,PRE_TOPC:def 5;
end;
given C being Subset of T such that
A2: C is open & C /\ [#](A) = B;
C in the topology of T & C /\ [#] A = B by A2,PRE_TOPC:def 5;
then B in the topology of A by PRE_TOPC:def 9;
hence B is open by PRE_TOPC:def 5;
end;
theorem Th33:
Q is open implies
for P being Subset of A st P=Q holds P is open
proof
assume A1: Q is open;
let P be Subset of A;
assume A2: P=Q;
P c= [#] A by PRE_TOPC:14;
then Q /\ [#] A = P by A2,XBOOLE_1:28;
hence thesis by A1,Th32;
end;
theorem Th34:
Q is closed implies
for P being Subset of A st P=Q holds P is closed
proof
assume A1: Q is closed;
let P be Subset of A such that A2: P=Q;
P c= [#] A by PRE_TOPC:14;
then Q /\ [#] A = P by A2,XBOOLE_1:28;
hence P is closed by A1,PRE_TOPC:43;
end;
theorem
F is open implies for G being Subset-Family of A st G=F holds
G is open
proof
assume A1: F is open;
let G be Subset-Family of A;
assume A2: G=F;
let P be Subset of A such that A3: P in G;
reconsider PP=P as Subset of T by PRE_TOPC:39;
PP is open by A1,A2,A3,Def1;
hence thesis by Th33;
end;
theorem
F is closed implies for G being Subset-Family of A st G=F
holds G is closed
proof
assume A1: F is closed;
let G be Subset-Family of A;
assume A2: G=F;
let P be Subset of A such that A3: P in G;
reconsider PP=P as Subset of T by PRE_TOPC:39;
PP is closed by A1,A2,A3,Def2;
hence thesis by Th34;
end;
canceled;
theorem Th38:
M /\ N is Subset of T|N
proof
M /\ N c= N by XBOOLE_1:17;
then M /\ N c= [#](T|N) by PRE_TOPC:def 10;
then M /\ N is Subset of T|N by PRE_TOPC:12;
hence M /\ N is Subset of T|N;
end;
::
:: RESTRICTION OF A FAMILY
::
definition
let T be TopStruct, P be Subset of T,
F be Subset-Family of T;
func F|P -> Subset-Family of T|P means
:Def3: for Q being Subset of T|P holds
Q in it iff
ex R being Subset of T
st R in F & R /\ P = Q;
existence
proof
thus ex G being Subset-Family of T|P st
(for Q being Subset of T|P holds Q in G iff
ex R being Subset of T st R in F & R /\ P = Q)
proof
defpred X[Subset of T|P] means
ex R being Subset of T st R in F & R /\ P = $1;
ex G being Subset-Family of T|P st
for Q being Subset of T|P holds Q in G iff X[Q]
from SubFamExS;
hence thesis;
end;
end;
uniqueness
proof
thus for G,H being Subset-Family of T|P st
(for Q being Subset of T|P holds Q in G iff
ex R being Subset of T st R in F & R /\ P = Q) &
(for Q being Subset of T|P holds Q in H iff
ex R being Subset of T st R in F & R /\ P = Q)
holds G = H
proof
let G,H be Subset-Family of T|P such that
A1: for Q being Subset of T|P holds Q in G iff
ex R being Subset of T st R in F & R /\ P = Q
and
A2: for Q being Subset of T|P holds Q in H iff
ex R being Subset of T st R in F & R /\ P = Q;
x in G iff x in H
proof
hereby assume A3: x in G;
then reconsider X=x as Subset of T|P;
ex R being Subset of T st R in
F & R /\ P = X by A1,A3
;
hence x in H by A2;
end;
assume A4: x in H;
then reconsider X=x as Subset of T|P;
ex R being Subset of T st R in F & R /\
P = X by A2,A4;
hence thesis by A1;
end;
hence thesis by TARSKI:2;
end;
end;
end;
canceled;
theorem
F c= G implies F|M c= G|M
proof
assume A1: F c= G;
let x;
assume A2: x in F|M;
then reconsider X=x as Subset of T|M;
consider R being Subset of T such that
A3: R in F & R /\ M = X by A2,Def3;
thus thesis by A1,A3,Def3;
end;
theorem Th41:
Q in F implies Q /\ M in F|M
proof
reconsider QQ = Q /\ M as Subset of T|M by Th38;
assume Q in F;
then Q in F & Q /\ M = QQ;
hence Q /\ M in F|M by Def3;
end;
theorem
Q c= union F implies Q /\ M c= union(F|M)
proof
assume A1: Q c= union F;
now assume M <> {};
thus Q /\ M c= union(F|M)
proof
let x; assume x in Q /\ M;
then A2: x in Q & x in M by XBOOLE_0:def 3;
then consider Z being set such that
A3: x in Z and A4: Z in F by A1,TARSKI:def 4;
reconsider ZZ=Z as Subset of T by A4;
ZZ /\ M in F|M by A4,Th41;
then reconsider ZP = ZZ /\ M as Subset of T|M;
x in ZP & ZP in F|M by A2,A3,A4,Th41,XBOOLE_0:def 3;
hence thesis by TARSKI:def 4;
end;
end;
hence thesis by XBOOLE_1:2;
end;
theorem
M c= union F implies M = union (F|M)
proof
assume A1: M c= union F;
x in M iff x in union(F|M)
proof
hereby assume A2: x in M;
then consider A being set such that
A3: x in A and A4:A in F by A1,TARSKI:def 4;
reconsider A'=A as Subset of T by A4;
A5: x in A /\ M by A2,A3,XBOOLE_0:def 3;
A /\ M c= M by XBOOLE_1:17;
then A /\ M c= [#](T|M) by PRE_TOPC:def 10;
then reconsider B=A' /\
M as Subset of T|M by PRE_TOPC:12;
B in F|M by A4,Def3;
hence x in union(F|M) by A5,TARSKI:def 4;
end;
assume x in union(F|M);
then consider A being set such that A6: x in A and A7: A in F|M
by TARSKI:def 4;
reconsider B = A as Subset of T|M by A7;
ex R being Subset of T st R in F & R /\ M = B by A7,
Def3
;
hence thesis by A6,XBOOLE_0:def 3;
end;
hence thesis by TARSKI:2;
end;
theorem Th44:
union(F|M) c= union F
proof
let x; assume x in union(F|M);
then consider A being set such that A1: x in A and A2: A in F|M by TARSKI:
def 4;
reconsider Q = A as Subset of T|M by A2;
consider R being Subset of T such that
A3: R in F and A4: R /\ M = Q by A2,Def3;
x in R & R in F by A1,A3,A4,XBOOLE_0:def 3;
hence thesis by TARSKI:def 4;
end;
theorem
M c= union (F|M) implies M c= union F
proof
assume M c= union(F|M);
then M c= union(F|M) & union(F|M) c= union F by Th44;
hence thesis by XBOOLE_1:1;
end;
theorem
F is finite implies F|M is finite
proof
assume A1: F is finite;
defpred X[set,set] means
for X being Subset of T st X = $1 holds $2 = X /\ M;
A2: for x,y1,y2 being set st x in F & X[x,y1] & X[x,y2]
holds y1 = y2
proof
let x,y1,y2 be set such that A3: x in F and
A4: for X being Subset of T st X = x
holds y1 = X /\ M and
A5: for X being Subset of T st X = x holds y2 = X /\ M;
reconsider X=x as Subset of T by A3;
y1 = X /\ M by A4;
hence thesis by A5;
end;
A6: for x st x in F ex y st X[x,y]
proof
let x; assume x in F;
then reconsider X=x as Subset of T;
reconsider y=X /\ M as set;
take y;
thus thesis;
end;
consider f being Function such that A7: dom f = F and
A8: for x st x in F holds X[x,f.x] from FuncEx(A2,A6);
x in rng f iff x in F|M
proof
hereby assume x in rng f;
then consider y such that A9: y in dom f and A10: x=f.y by FUNCT_1:def
5;
reconsider Y=y as Subset of T by A7,A9;
A11: f.y = Y /\ M by A7,A8,A9;
Y /\ M c= M by XBOOLE_1:17;
then Y /\ M c= [#](T|M) by PRE_TOPC:def 10;
then reconsider X=f.y as Subset of T|M
by A11,PRE_TOPC:12;
X in F|M by A7,A9,A11,Def3;
hence x in F|M by A10;
end;
assume A12: x in F|M;
then reconsider X=x as Subset of T|M;
consider R being Subset of T such that
A13: R in F and A14: R /\ M = X by A12,Def3;
f.R = R /\ M by A8,A13;
hence x in rng f by A7,A13,A14,FUNCT_1:def 5;
end;
then rng f = F|M by TARSKI:2;
then f.:(F) = F|M by A7,RELAT_1:146;
hence thesis by A1,FINSET_1:17;
end;
theorem
F is open implies F|M is open
proof
assume that A1: F is open;
let Q be Subset of T|M;
assume Q in F|M;
then consider R being Subset of T such that
A2: R in F and A3: R /\ M = Q by Def3;
reconsider R as Subset of T;
A4: R is open by A1,A2,Def1;
Q = R /\ [#](T|M) by A3,PRE_TOPC:def 10;
hence thesis by A4,Th32;
end;
theorem
F is closed implies F|M is closed
proof
assume that A1: F is closed;
let Q be Subset of T|M;
assume Q in F|M;
then consider R being Subset of T such that
A2: R in F and A3: R /\ M = Q by Def3;
reconsider R as Subset of T;
A4: R is closed by A1,A2,Def2;
Q = R /\ [#](T|M) by A3,PRE_TOPC:def 10;
hence thesis by A4,PRE_TOPC:43;
end;
theorem
for F being Subset-Family of A st F is open
ex G being Subset-Family of T st G is open &
for AA being Subset of T st AA = [#] A holds F = G|AA
proof
let F be Subset-Family of A;
[#] A c= [#]T by PRE_TOPC:def 9;
then reconsider At = [#] A as Subset of T by PRE_TOPC:12;
assume A1: F is open;
defpred X[Subset of T] means
ex X1 being Subset of T st X1 = $1 & X1 is open & $1 /\ At in F;
consider G being Subset-Family of T such that
A2: for X being Subset of T holds X in G iff X[X]
from SubFamExS;
take G;
thus G is open
proof
let H be Subset of T; assume H in G;
then ex X1 being Subset of T st X1 = H & X1 is open & H /\ At in F by
A2;
hence thesis;
end;
let AA be Subset of T; assume
A3: AA = [#] A;
then F c= bool AA by Th1;
then F c= bool [#](T|AA) by PRE_TOPC:def 10;
then F c= bool the carrier of (T|AA) by PRE_TOPC:12;
then F is Subset-Family of T|AA by SETFAM_1:def 7;
then reconsider FF = F as Subset-Family of T|AA;
for X being Subset of T|AA holds X in FF iff
ex X' being Subset of T st X' in G & X' /\ AA=X
proof
let X be Subset of T|AA;
thus X in FF implies
ex X' being Subset of T st X' in G & X' /\ AA=X
proof
assume A4: X in FF;
then reconsider XX=X as Subset of A;
XX is open by A1,A4,Def1;
then consider Y being Subset of T such that
A5: Y is open and A6: Y /\ [#] A = XX by Th32;
take X' = Y;
thus X' in G & X' /\ AA=X by A2,A3,A4,A5,A6;
end;
given X' being Subset of T such that
A7: X' in G & X' /\ AA=X;
ex X1 being Subset of T st X1 = X' & X1 is open & X' /\ At in F
by A2,A7;
hence thesis by A3,A7;
end;
hence thesis by Def3;
end;
theorem
ex f being Function st dom f = F & rng f = F|P &
for x st x in F for Q st Q = x holds f.x = Q /\ P
proof
defpred X[set,set] means for Q st Q=$1 holds $2=Q /\ P;
A1: for x,y1,y2 being set st x in F & X[x,y1] & X[x,y2]
holds y1 = y2
proof
let x,y1,y2 be set;
assume that A2: x in F and A3: for Q st Q=x holds y1=Q /\ P
and A4: for Q st Q=x holds y2=Q /\ P;
reconsider Q=x as Subset of T by A2;
y1=Q /\ P by A3;
hence thesis by A4;
end;
A5: for x st x in F ex y st X[x,y]
proof
let x; assume x in F;
then reconsider Q=x as Subset of T;
reconsider y=Q /\ P as set;
take y;
thus thesis;
end;
consider f being Function such that
A6: dom f = F and
A7: for x st x in F holds X[x,f.x] from FuncEx(A1,A5);
take f;
thus dom f = F by A6;
x in rng f iff x in F|P
proof
hereby assume x in rng f;
then consider y such that
A8: y in dom f and A9: f.y=x by FUNCT_1:def 5;
reconsider Y=y as Subset of T by A6,A8;
A10: x = Y /\ P by A6,A7,A8,A9;
Y /\ P c= P by XBOOLE_1:17;
then Y /\ P c= [#](T|P) by PRE_TOPC:def 10;
then reconsider X=x as Subset of T|P by A10,PRE_TOPC:12;
Y in F & X = Y /\ P by A6,A7,A8,A9;
hence x in F|P by Def3;
end;
assume A11: x in F|P;
then reconsider X=x as Subset of T|P;
consider Q be Subset of T such that
A12: Q in F and A13: Q /\ P = X by A11,Def3;
reconsider p=Q as set;
p in dom f & f.p = x by A6,A7,A12,A13;
hence thesis by FUNCT_1:def 5;
end;
hence rng f = F|P by TARSKI:2;
thus for x st x in F for Q st Q = x holds f.x = Q /\ P by A7;
end;
::
:: MAPPING OF THE TOPOLOGICAL SPACES
::
theorem Th51:
for T being 1-sorted, S being non empty 1-sorted,
f being map of T, S holds
dom f = [#]T & rng f c= [#]S
proof
let T be 1-sorted, S be non empty 1-sorted,
f be map of T, S;
dom f = the carrier of T &
rng f c= the carrier of S by FUNCT_2:def 1,RELSET_1:12;
hence thesis by PRE_TOPC:12;
end;
theorem Th52:
for T being 1-sorted, S being non empty 1-sorted,
f being map of T, S holds
f"([#]S) = [#]T
proof
let T be 1-sorted, S be non empty 1-sorted,
f be map of T, S;
A1: f"(rng f) = dom f by RELAT_1:169
.= [#]T by Th51;
rng f c= [#]S by Th51;
then [#]T c= f"([#]S) & f"([#]S) c= dom f by A1,RELAT_1:167,178;
then [#]T c= f"([#]S) & f"([#]S) c= [#]T by Th51;
hence thesis by XBOOLE_0:def 10;
end;
canceled;
theorem
for T being 1-sorted, S being non empty 1-sorted,
f being map of T, S,
H being Subset-Family of S holds
("f).:H is Subset-Family of T
proof
let T be 1-sorted, S be non empty 1-sorted,
f be map of T, S,
H be Subset-Family of S;
A1: ("f).:H c= rng "f by RELAT_1:144;
rng "f c= bool dom f by FUNCT_3:25;
then ("f).:H c= bool dom f by A1,XBOOLE_1:1;
then ("f).:H is Subset of bool [#]T & [#]T = the carrier of T
by Th51,PRE_TOPC:12;
then ("f).:H is Subset-Family of T by SETFAM_1:def 7;
hence thesis;
end;
::
:: CONTINUOUS MAPPING
::
reserve S, V for non empty TopStruct,
f for map of T, S,
g for map of S, V,
H for Subset-Family of S,
P1 for Subset of S;
theorem Th55:
f is continuous iff
(for P1 st P1 is open holds f"P1 is open)
proof
hereby assume A1: f is continuous;
let P1; assume P1 is open;
then P1` is closed by TOPS_1:30;
then A2: f"(P1`) is closed by A1,PRE_TOPC:def 12;
f"(P1`) = f"([#]S \ P1) by PRE_TOPC:17
.= f"([#]S) \ f"P1 by FUNCT_1:138
.= [#]T \ f"P1 by Th52
.= (f"P1)` by PRE_TOPC:17;
hence f"P1 is open by A2,TOPS_1:30;
end;
assume A3: for P1 st P1 is open holds f"P1 is open;
let P1; assume P1 is closed;
then P1` is open by TOPS_1:29;
then A4: f"(P1`) is open by A3;
f"(P1`) = f"([#]S \ P1) by PRE_TOPC:17
.= f"([#]S) \ f"P1 by FUNCT_1:138
.= [#]T \ f"P1 by Th52
.= (f"P1)` by PRE_TOPC:17;
hence thesis by A4,TOPS_1:29;
end;
theorem Th56:
for T being TopSpace, S being non empty TopSpace, f being map of T, S holds
f is continuous iff
for P1 being Subset of S holds Cl(f"P1) c= f"(Cl P1)
proof
let T be TopSpace, S be non empty TopSpace, f be map of T, S;
hereby assume A1: f is continuous;
let P1 be Subset of S;
P1 c= Cl P1 by PRE_TOPC:48;
then f"P1 c= f"(Cl P1) by RELAT_1:178;
then A2: Cl(f"P1) c= Cl(f"(Cl P1)) by PRE_TOPC:49;
Cl(Cl P1) = Cl P1 by TOPS_1:26;
then Cl P1 is closed by PRE_TOPC:52;
then f"(Cl P1) is closed by A1,PRE_TOPC:def 12;
hence Cl(f"P1) c= f"(Cl P1) by A2,PRE_TOPC:52;
end;
assume A3:for P1 being Subset of S
holds Cl(f"P1) c= f"(Cl P1);
let P1 be Subset of S; assume P1 is closed;
then Cl P1 = P1 by PRE_TOPC:52;
then f"P1 c= Cl(f"P1) & Cl(f"P1) c= f"P1 by A3,PRE_TOPC:48;
then f"P1 = Cl(f"P1) by XBOOLE_0:def 10;
hence f"P1 is closed by PRE_TOPC:52;
end;
theorem Th57:
for T being TopSpace, S being non empty TopSpace, f being map of T, S holds
f is continuous iff
for P being Subset of T holds f.:(Cl P) c= Cl(f.:P)
proof
let T be TopSpace, S be non empty TopSpace, f be map of T, S;
hereby assume A1: f is continuous;
let P be Subset of T;
A2: Cl(f"(f.:P)) c= f"(Cl(f.:P)) by A1,Th56;
P c= [#]T by PRE_TOPC:14;
then P c= dom f by Th51;
then P c= f"(f.:P) by FUNCT_1:146;
then Cl P c= Cl(f"(f.:P)) by PRE_TOPC:49;
then Cl P c= f"(Cl(f.:P)) by A2,XBOOLE_1:1;
then A3: f.:(Cl P) c= f.:(f"(Cl(f.:P))) by RELAT_1:156;
f.:(f"(Cl(f.:P))) c= Cl(f.:P) by FUNCT_1:145;
hence f.:(Cl P) c= Cl(f.:P) by A3,XBOOLE_1:1;
end;
assume A4: for P being Subset of T holds f.:(Cl P) c= Cl(f.:
P);
now let P1 be Subset of S;
Cl(f"P1) c= [#]T by PRE_TOPC:14;
then Cl(f"P1) c= dom f by Th51;
then A5: Cl(f"P1) c= f"(f.:Cl(f"P1)) by FUNCT_1:146;
f.:(f"P1) c= P1 by FUNCT_1:145;
then f.:(Cl(f"P1)) c= Cl(f.:(f"P1)) &
Cl(f.:(f"P1)) c= Cl P1 by A4,PRE_TOPC:49;
then f.:(Cl(f"P1)) c= Cl P1 by XBOOLE_1:1;
then f"(f.:(Cl(f"P1))) c= f"(Cl P1) by RELAT_1:178;
hence Cl(f"P1) c= f"(Cl P1) by A5,XBOOLE_1:1;
end;
hence thesis by Th56;
end;
theorem Th58:
f is continuous & g is continuous implies g*f is continuous
proof
assume that A1: f is continuous and A2: g is continuous;
let P be Subset of V;
A3: (g*f)"P = f"(g"P) by RELAT_1:181;
assume P is closed;
then g"P is closed by A2,PRE_TOPC:def 12;
hence thesis by A1,A3,PRE_TOPC:def 12;
end;
theorem
f is continuous & H is open implies
for F st F=("f).:H holds F is open
proof
assume that A1: f is continuous and A2: H is open;
let F such that A3: F=("f).:H;
let X be Subset of T; assume X in F;
then consider y being set such that A4: y in dom "f and A5: y in H and
A6: X=("f).y by A3,FUNCT_1:def 12;
reconsider Y=y as Subset of S by A5;
A7: X = f"Y by A4,A6,FUNCT_3:24;
Y is open by A2,A5,Def1; hence thesis by A1,A7,Th55;
end;
theorem
for T, S being TopStruct, f being map of T, S,
H being Subset-Family of S st
f is continuous & H is closed holds
for F being Subset-Family of T st F=("f).:H holds F is closed
proof
let T, S be TopStruct, f be map of T, S,
H be Subset-Family of S;
assume that A1: f is continuous and A2: H is closed;
let F be Subset-Family of T such that A3: F=("f).:H;
let X be Subset of T; assume X in F;
then consider y being set such that A4: y in dom "f and A5: y in H and
A6: X=("f).y by A3,FUNCT_1:def 12;
reconsider Y=y as Subset of S by A5;
A7: X = f"Y by A4,A6,FUNCT_3:24;
Y is closed by A2,A5,Def2; hence thesis by A1,A7,PRE_TOPC:def 12;
end;
definition let T, S be 1-sorted, f be map of T,S;
assume that
A1: rng f = [#]S and
A2: f is one-to-one;
func f/" -> map of S,T equals
:Def4: f";
coherence
proof
rng f = the carrier of S by A1,PRE_TOPC:12;
then f" is Function of the carrier of S, the carrier of T
by A2,FUNCT_2:31;
hence f" is map of S,T;
end;
synonym f";
end;
canceled;
theorem Th62:
for T being 1-sorted, S being non empty 1-sorted, f being map of T,S st
rng f = [#]S & f is one-to-one holds
dom(f") = [#]S & rng(f") = [#]T
proof
let T be 1-sorted, S be non empty 1-sorted, f be map of T,S;
assume A1: rng f = [#]S & f is one-to-one;
hence dom(f") = dom((f qua Function)") by Def4
.= [#]S by A1,FUNCT_1:54;
thus rng(f") = rng((f qua Function)") by A1,Def4
.= dom f by A1,FUNCT_1:55
.= [#]T by Th51;
end;
theorem Th63:
for T, S being 1-sorted, f being map of T,S st
rng f = [#]S & f is one-to-one holds f" is one-to-one
proof
let T, S be 1-sorted, f be map of T,S;
assume A1: rng f = [#]S & f is one-to-one;
then (f qua Function)" is one-to-one by FUNCT_1:62;
hence f" is one-to-one by A1,Def4;
end;
theorem Th64:
for T being 1-sorted, S being non empty 1-sorted, f being map of T,S st
rng f = [#]S & f is one-to-one holds (f")" = f
proof
let T be 1-sorted, S be non empty 1-sorted, f be map of T,S;
assume A1: rng f = [#]S & f is one-to-one;
then f = ((f qua Function)")"
by FUNCT_1:65;
then A2: f = (f" qua Function)"
by A1,Def4;
dom(f") = [#]S & rng(f") = [#]T & f" is one-to-one by A1,Th62,Th63;
hence thesis by A2,Def4;
end;
theorem
for T, S being 1-sorted, f being map of T,S st
rng f = [#]S & f is one-to-one holds
f"*f = id dom f & f*f" = id rng f
proof
let T, S be 1-sorted, f be map of T,S;
assume A1: rng f = [#]S & f is one-to-one;
then (f qua Function)"*f = id dom f
& f*(f qua Function)" = id rng f by FUNCT_1:61;
hence thesis by A1,Def4;
end;
theorem Th66:
for T being 1-sorted, S, V being non empty 1-sorted,
f being map of T,S, g being map of S,V st
dom f = [#]T & rng f = [#]S & f is one-to-one &
dom g = [#]S & rng g = [#]V & g is one-to-one
holds (g*f)" = f"*g"
proof
let T be 1-sorted, S, V be non empty 1-sorted;
let f be map of T,S;
let g be map of S,V;
assume A1: dom f = [#]T &
rng f = [#]S & f is one-to-one;
assume A2: dom g = [#]S &
rng g = [#] V & g is one-to-one;
then dom(g*f) = [#]T & rng(g*f) = [#] V & g*f is one-to-one
by A1,FUNCT_1:46,RELAT_1:46,47;
then f" = (f qua Function)" &
g" = (g qua Function)" &
(g*f)" = ((g*f) qua Function)"
by A1,A2,Def4;
hence thesis by A1,A2,FUNCT_1:66;
end;
theorem Th67:
for T, S being 1-sorted, f being map of T, S,
P being Subset of T st
rng f = [#]S & f is one-to-one holds f.:P = (f")"P
proof
let T, S be 1-sorted, f be map of T, S,
P be Subset of T;
assume A1: rng f = [#]S & f is one-to-one;
then f.:P = ((f qua Function)")"P
by FUNCT_1:154;
hence thesis by A1,Def4;
end;
theorem Th68:
for T, S being 1-sorted, f being map of T,S,
P1 being Subset of S st
rng f = [#]S & f is one-to-one holds f"P1 = (f").:P1
proof
let T, S be 1-sorted, f be map of T, S,
P1 be Subset of S;
assume A1: rng f = [#]S & f is one-to-one;
then f"P1 = ((f qua Function)").:P1 by FUNCT_1:155;
hence thesis by A1,Def4;
end;
::
:: HOMEOMORPHISM
::
definition let S, T be TopStruct, f be map of S, T;
attr f is being_homeomorphism means :Def5:
dom f = [#]S & rng f = [#]T & f is one-to-one &
f is continuous & f" is continuous;
synonym f is_homeomorphism;
end;
canceled;
theorem
f is_homeomorphism implies f" is_homeomorphism
proof
assume A1: f is_homeomorphism;
then A2: dom f = [#]T & rng f = [#](S) & f is one-to-one &
f is continuous & f" is continuous by Def5;
hence dom(f") = [#]S & rng (f") = [#](T) by Th62;
thus f" is one-to-one by A2,Th63;
thus f" is continuous by A1,Def5;
thus (f")" is continuous by A2,Th64;
end;
theorem
for T, S, V being non empty TopStruct,
f being map of T,S, g being map of S,V st
f is_homeomorphism & g is_homeomorphism holds g*f is_homeomorphism
proof
let T, S, V be non empty TopStruct;
let f be map of T,S;
let g be map of S,V;
assume that A1: f is_homeomorphism and A2: g is_homeomorphism;
A3: dom f = [#]T & rng f = [#](S) & f is one-to-one &
f is continuous & f" is continuous by A1,Def5;
A4: dom g = [#]S & rng g = [#](V) & g is one-to-one &
g is continuous & g" is continuous by A2,Def5;
hence dom(g*f) = [#]T & rng(g*f) = [#] V by A3,RELAT_1:46,47;
thus g*f is one-to-one by A3,A4,FUNCT_1:46;
thus g*f is continuous by A3,A4,Th58;
f"*g" is continuous by A3,A4,Th58;
hence (g*f)" is continuous by A3,A4,Th66;
end;
theorem
f is_homeomorphism iff
dom f = [#]T & rng f = [#]S & f is one-to-one &
for P holds P is closed iff f.:P is closed
proof
hereby assume A1: f is_homeomorphism;
then A2: f is continuous by Def5;
thus A3: dom f = [#]T & rng f = [#]S & f is one-to-one by A1,Def5;
A4: f" is continuous by A1,Def5;
let P;
hereby assume A5: P is closed;
(f")"P = ((f qua Function)")"P
by A3,Def4
.= f.:P by A3,FUNCT_1:154;
hence f.:P is closed by A4,A5,PRE_TOPC:def 12;
end;
assume f.:P is closed;
then A6: f"(f.:P) is closed by A2,PRE_TOPC:def 12;
A7: f"(f.:P) c= P by A3,FUNCT_1:152;
dom f = [#]T by Th51;
then P c= dom f by PRE_TOPC:14;
then P c= f"(f.:P) by FUNCT_1:146;
hence P is closed by A6,A7,XBOOLE_0:def 10;
end;
assume
A8: dom f = [#]T & rng f = [#]S & f is one-to-one;
assume A9: for P being Subset of T holds
P is closed iff f.:P is closed;
A10: f is continuous
proof
let B be Subset of S such that A11: B is closed;
set D = f"B;
B c= rng f by A8,PRE_TOPC:14;
then B = f.:D by FUNCT_1:147;
hence D is closed by A9,A11;
end;
f" is continuous
proof
let B be Subset of T such that
A12: B is closed;
(f")"B = ((f qua Function)")"B by A8,Def4
.= f.:B by A8,FUNCT_1:154;
hence thesis by A9,A12;
end;
hence thesis by A8,A10,Def5;
end;
reserve T, S for non empty TopSpace,
P for Subset of T,
P1 for Subset of S,
f for map of T, S;
theorem
f is_homeomorphism iff
dom f = [#]T & rng f = [#]S & f is one-to-one &
for P1 holds f"(Cl P1) = Cl(f"P1)
proof
hereby assume A1: f is_homeomorphism;
hence A2: dom f = [#]T & rng f = [#]S & f is one-to-one by Def5;
let P1;
f is continuous by A1,Def5;
then A3: Cl(f"P1) c= f"(Cl P1) by Th56;
f" is continuous by A1,Def5;
then A4: (f").:(Cl P1) c= Cl((f").:P1) by Th57;
f"(Cl P1) = (f").:(Cl P1) & f"P1 = (f").:P1 by A2,Th68;
hence f"(Cl P1) = Cl(f"P1) by A3,A4,XBOOLE_0:def 10;
end;
assume that A5: dom f = [#]T & rng f = [#]S and A6: f is one-to-one;
assume A7: for P1 holds f"(Cl P1) = Cl(f"P1);
thus dom f = [#]T & rng f = [#]S & f is one-to-one by A5,A6;
for P1 holds Cl(f"P1) c= f"(Cl P1) by A7;
hence f is continuous by Th56;
now let P1;
(f").:(Cl P1) = f"(Cl P1) & (f").:P1 = f"P1 by A5,A6,Th68;
hence (f").:(Cl P1) c= Cl((f").:P1) by A7;
end;
hence f" is continuous by Th57;
end;
theorem
f is_homeomorphism iff
dom f = [#]T & rng f = [#]
S & f is one-to-one & for P holds f.:(Cl P) = Cl(f.:P)
proof
hereby assume
A1: f is_homeomorphism;
then A2: f is continuous & f" is continuous by Def5;
thus A3: dom f = [#]T & rng f = [#]S & f is one-to-one by A1,Def5;
let P;
A4: f.:(Cl P) c= Cl(f.:P) by A2,Th57;
A5: Cl((f")"P) c= (f")"(Cl P) by A2,Th56;
(f")"P = f.:P & (f")"(Cl P) = f.:(Cl P) by A3,Th67;
hence f.:(Cl P) = Cl(f.:P) by A4,A5,XBOOLE_0:def 10;
end;
assume A6: dom f = [#]T & rng f = [#]S & f is one-to-one;
assume A7: for P holds f.:(Cl P) = Cl(f.:P);
thus dom f = [#]T & rng f = [#]S & f is one-to-one by A6;
for P holds f.:(Cl P) c= Cl(f.:P) by A7;
hence f is continuous by Th57;
now let P;
(f")"P = f.:P & (f")"(Cl P) = f.:(Cl P) by A6,Th67;
hence Cl((f")"P) c= (f")"(Cl P) by A7;
end;
hence f" is continuous by Th56;
end;