Volume 4, 1992

University of Bialystok

Copyright (c) 1992 Association of Mizar Users

### The abstract of the Mizar article:

### Separated and Weakly Separated Subspaces of Topological Spaces

**by****Zbigniew Karno**- Received January 8, 1992
- MML identifier: TSEP_1

- [ Mizar article, MML identifier index ]

environ vocabulary BOOLE, PRE_TOPC, SUBSET_1, RELAT_1, TARSKI, SETFAM_1, CONNSP_1, TSEP_1; notation TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC, CONNSP_1, BORSUK_1; constructors CONNSP_1, BORSUK_1, MEMBERED; clusters PRE_TOPC, BORSUK_1, STRUCT_0, COMPLSP1, SUBSET_1, TOPS_1, MEMBERED, ZFMISC_1; requirements BOOLE, SUBSET; begin ::1. Some Properties of Subspaces of Topological Spaces. reserve X for TopSpace; theorem :: TSEP_1:1 for X being TopStruct, X0 being SubSpace of X holds the carrier of X0 is Subset of X; theorem :: TSEP_1:2 for X being TopStruct holds X is SubSpace of X; theorem :: TSEP_1:3 for X being strict TopStruct holds X|[#]X = X; theorem :: TSEP_1:4 for X1, X2 being SubSpace of X holds the carrier of X1 c= the carrier of X2 iff X1 is SubSpace of X2; theorem :: TSEP_1:5 for X being TopStruct for X1, X2 being SubSpace of X st the carrier of X1 = the carrier of X2 holds the TopStruct of X1 = the TopStruct of X2; theorem :: TSEP_1:6 for X1, X2 being SubSpace of X st X1 is SubSpace of X2 & X2 is SubSpace of X1 holds the TopStruct of X1 = the TopStruct of X2; theorem :: TSEP_1:7 for X1 being SubSpace of X for X2 being SubSpace of X1 holds X2 is SubSpace of X; theorem :: TSEP_1:8 for X0 being SubSpace of X, C, A being Subset of X, B being Subset of X0 st C is closed & C c= the carrier of X0 & A c= C & A = B holds B is closed iff A is closed; theorem :: TSEP_1:9 for X0 being SubSpace of X, C, A being Subset of X, B being Subset of X0 st C is open & C c= the carrier of X0 & A c= C & A = B holds B is open iff A is open; theorem :: TSEP_1:10 for X being non empty TopStruct, A0 being non empty Subset of X ex X0 being strict non empty SubSpace of X st A0 = the carrier of X0; ::Properties of Closed Subspaces (for the definition see BORSUK_1:def 13). theorem :: TSEP_1:11 for X0 being SubSpace of X, A being Subset of X st A = the carrier of X0 holds X0 is closed SubSpace of X iff A is closed; theorem :: TSEP_1:12 for X0 being closed SubSpace of X, A being Subset of X, B being Subset of X0 st A = B holds B is closed iff A is closed; theorem :: TSEP_1:13 for X1 being closed SubSpace of X, X2 being closed SubSpace of X1 holds X2 is closed SubSpace of X; theorem :: TSEP_1:14 for X being non empty TopSpace, X1 being closed non empty SubSpace of X, X2 being non empty SubSpace of X st the carrier of X1 c= the carrier of X2 holds X1 is closed non empty SubSpace of X2; theorem :: TSEP_1:15 for X be non empty TopSpace, A0 being non empty Subset of X st A0 is closed ex X0 being strict closed non empty SubSpace of X st A0 = the carrier of X0; definition let X be TopStruct; let IT be SubSpace of X; attr IT is open means :: TSEP_1:def 1 for A being Subset of X st A = the carrier of IT holds A is open; end; definition let X be TopSpace; cluster strict open SubSpace of X; end; definition let X be non empty TopSpace; cluster strict open non empty SubSpace of X; end; ::Properties of Open Subspaces. theorem :: TSEP_1:16 for X0 being SubSpace of X, A being Subset of X st A = the carrier of X0 holds X0 is open SubSpace of X iff A is open; theorem :: TSEP_1:17 for X0 being open SubSpace of X, A being Subset of X, B being Subset of X0 st A = B holds B is open iff A is open; theorem :: TSEP_1:18 for X1 being open SubSpace of X, X2 being open SubSpace of X1 holds X2 is open SubSpace of X; theorem :: TSEP_1:19 for X be non empty TopSpace, X1 being open SubSpace of X, X2 being non empty SubSpace of X st the carrier of X1 c= the carrier of X2 holds X1 is open SubSpace of X2; theorem :: TSEP_1:20 for X be non empty TopSpace, A0 being non empty Subset of X st A0 is open ex X0 being strict open non empty SubSpace of X st A0 = the carrier of X0; begin ::2. Operations on Subspaces of Topological Spaces. reserve X for non empty TopSpace; definition let X be non empty TopStruct; let X1, X2 be non empty SubSpace of X; func X1 union X2 -> strict non empty SubSpace of X means :: TSEP_1:def 2 the carrier of it = (the carrier of X1) \/ (the carrier of X2); commutativity; end; reserve X1, X2, X3 for non empty SubSpace of X; ::Properties of the Union of two Subspaces. theorem :: TSEP_1:21 (X1 union X2) union X3 = X1 union (X2 union X3); theorem :: TSEP_1:22 X1 is SubSpace of X1 union X2; theorem :: TSEP_1:23 for X1,X2 being non empty SubSpace of X holds X1 is SubSpace of X2 iff X1 union X2 = the TopStruct of X2; theorem :: TSEP_1:24 for X1, X2 being closed non empty SubSpace of X holds X1 union X2 is closed SubSpace of X; theorem :: TSEP_1:25 for X1, X2 being open non empty SubSpace of X holds X1 union X2 is open SubSpace of X; definition let X be TopStruct; let X1, X2 be SubSpace of X; pred X1 misses X2 means :: TSEP_1:def 3 the carrier of X1 misses the carrier of X2; symmetry; antonym X1 meets X2; end; definition let X be non empty TopStruct; let X1, X2 be non empty SubSpace of X; assume X1 meets X2; canceled; func X1 meet X2 -> strict non empty SubSpace of X means :: TSEP_1:def 5 the carrier of it = (the carrier of X1) /\ (the carrier of X2); end; reserve X1, X2, X3 for non empty SubSpace of X; ::Properties of the Meet of two Subspaces. canceled 3; theorem :: TSEP_1:29 (X1 meets X2 implies X1 meet X2 = X2 meet X1) & ((X1 meets X2 & (X1 meet X2) meets X3 or X2 meets X3 & X1 meets (X2 meet X3)) implies (X1 meet X2) meet X3 = X1 meet (X2 meet X3)); theorem :: TSEP_1:30 X1 meets X2 implies X1 meet X2 is SubSpace of X1 & X1 meet X2 is SubSpace of X2; theorem :: TSEP_1:31 for X1,X2 being non empty SubSpace of X holds X1 meets X2 implies (X1 is SubSpace of X2 iff X1 meet X2 = the TopStruct of X1) & (X2 is SubSpace of X1 iff X1 meet X2 = the TopStruct of X2); theorem :: TSEP_1:32 for X1, X2 being closed non empty SubSpace of X st X1 meets X2 holds X1 meet X2 is closed SubSpace of X; theorem :: TSEP_1:33 for X1, X2 being open non empty SubSpace of X st X1 meets X2 holds X1 meet X2 is open SubSpace of X; ::Connections between the Union and the Meet. theorem :: TSEP_1:34 X1 meets X2 implies X1 meet X2 is SubSpace of X1 union X2; theorem :: TSEP_1:35 for Y being non empty SubSpace of X st X1 meets Y & Y meets X2 holds (X1 union X2) meet Y = (X1 meet Y) union (X2 meet Y) & Y meet (X1 union X2) = (Y meet X1) union (Y meet X2); theorem :: TSEP_1:36 for Y being non empty SubSpace of X holds X1 meets X2 implies (X1 meet X2) union Y = (X1 union Y) meet (X2 union Y) & Y union (X1 meet X2) = (Y union X1) meet (Y union X2); begin ::3. Separated and Weakly Separated Subsets of Topological Spaces. definition let X be TopStruct, A1, A2 be Subset of X; redefine ::for the previous definition see CONNSP_1:def 1 pred A1,A2 are_separated; antonym A1,A2 are_not_separated; end; reserve X for TopSpace; reserve A1, A2 for Subset of X; ::Properties of Separated Subsets of Topological Spaces. theorem :: TSEP_1:37 for A1,A2 being Subset of X holds A1,A2 are_separated implies A1 misses A2; theorem :: TSEP_1:38 A1 is closed & A2 is closed implies (A1 misses A2 iff A1,A2 are_separated); theorem :: TSEP_1:39 A1 \/ A2 is closed & A1,A2 are_separated implies A1 is closed & A2 is closed; theorem :: TSEP_1:40 A1 misses A2 & A1 is open implies A1 misses Cl A2; theorem :: TSEP_1:41 A1 is open & A2 is open implies (A1 misses A2 iff A1,A2 are_separated); theorem :: TSEP_1:42 A1 \/ A2 is open & A1,A2 are_separated implies A1 is open & A2 is open; ::A Restriction Theorem for Separated Subsets (see also CONNSP_1:8). reserve A1,A2 for Subset of X; theorem :: TSEP_1:43 for C being Subset of X holds A1,A2 are_separated implies A1 /\ C,A2 /\ C are_separated; theorem :: TSEP_1:44 for B being Subset of X holds A1,B are_separated or A2,B are_separated implies A1 /\ A2,B are_separated; theorem :: TSEP_1:45 for B being Subset of X holds A1,B are_separated & A2,B are_separated iff A1 \/ A2,B are_separated; theorem :: TSEP_1:46 A1,A2 are_separated iff ex C1, C2 being Subset of X st A1 c= C1 & A2 c= C2 & C1 misses A2 & C2 misses A1 & C1 is closed & C2 is closed; ::First Characterization of Separated Subsets of Topological Spaces. theorem :: TSEP_1:47 A1,A2 are_separated iff ex C1, C2 being Subset of X st A1 c= C1 & A2 c= C2 & C1 /\ C2 misses A1 \/ A2 & C1 is closed & C2 is closed; theorem :: TSEP_1:48 A1,A2 are_separated iff ex C1, C2 being Subset of X st A1 c= C1 & A2 c= C2 & C1 misses A2 & C2 misses A1 & C1 is open & C2 is open; ::Second Characterization of Separated Subsets of Topological Spaces. theorem :: TSEP_1:49 A1,A2 are_separated iff ex C1, C2 being Subset of X st A1 c= C1 & A2 c= C2 & C1 /\ C2 misses A1 \/ A2 & C1 is open & C2 is open; definition let X be TopStruct, A1, A2 be Subset of X; canceled; pred A1,A2 are_weakly_separated means :: TSEP_1:def 7 A1 \ A2,A2 \ A1 are_separated; symmetry; antonym A1,A2 are_not_weakly_separated; end; reserve X for TopSpace, A1, A2 for Subset of X; ::Properties of Weakly Separated Subsets of Topological Spaces. canceled; theorem :: TSEP_1:51 A1 misses A2 & A1,A2 are_weakly_separated iff A1,A2 are_separated; theorem :: TSEP_1:52 A1 c= A2 implies A1,A2 are_weakly_separated; theorem :: TSEP_1:53 for A1,A2 being Subset of X holds A1 is closed & A2 is closed implies A1,A2 are_weakly_separated; theorem :: TSEP_1:54 for A1,A2 being Subset of X holds A1 is open & A2 is open implies A1,A2 are_weakly_separated; ::Extension Theorems for Weakly Separated Subsets. theorem :: TSEP_1:55 for C being Subset of X holds A1,A2 are_weakly_separated implies A1 \/ C,A2 \/ C are_weakly_separated; theorem :: TSEP_1:56 for B1, B2 being Subset of X st B1 c= A2 & B2 c= A1 holds A1,A2 are_weakly_separated implies A1 \/ B1,A2 \/ B2 are_weakly_separated; theorem :: TSEP_1:57 for B being Subset of X holds A1,B are_weakly_separated & A2,B are_weakly_separated implies A1 /\ A2,B are_weakly_separated; theorem :: TSEP_1:58 for B being Subset of X holds A1,B are_weakly_separated & A2,B are_weakly_separated implies A1 \/ A2,B are_weakly_separated; ::First Characterization of Weakly Separated Subsets of Topological Spaces. theorem :: TSEP_1:59 A1,A2 are_weakly_separated iff ex C1, C2, C being Subset of X st C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2) \/ C & C1 is closed & C2 is closed & C is open ; reserve X for non empty TopSpace, A1, A2 for Subset of X; theorem :: TSEP_1:60 A1,A2 are_weakly_separated & not A1 c= A2 & not A2 c= A1 implies ex C1, C2 being non empty Subset of X st C1 is closed & C2 is closed & C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & (A1 \/ A2 c= C1 \/ C2 or ex C being non empty Subset of X st C is open & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2) \/ C); theorem :: TSEP_1:61 A1 \/ A2 = the carrier of X implies (A1,A2 are_weakly_separated iff ex C1, C2, C being Subset of X st A1 \/ A2 = (C1 \/ C2) \/ C & C1 c= A1 & C2 c= A2 & C c= A1 /\ A2 & C1 is closed & C2 is closed & C is open); theorem :: TSEP_1:62 A1 \/ A2 = the carrier of X & A1,A2 are_weakly_separated & not A1 c= A2 & not A2 c= A1 implies ex C1, C2 being non empty Subset of X st C1 is closed & C2 is closed & C1 c= A1 & C2 c= A2 & (A1 \/ A2 = C1 \/ C2 or ex C being non empty Subset of X st A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1 /\ A2 & C is open); ::Second Characterization of Weakly Separated Subsets of Topological Spaces. theorem :: TSEP_1:63 A1,A2 are_weakly_separated iff ex C1, C2, C being Subset of X st C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2) \/ C & C1 is open & C2 is open & C is closed; theorem :: TSEP_1:64 A1,A2 are_weakly_separated & not A1 c= A2 & not A2 c= A1 implies ex C1, C2 being non empty Subset of X st C1 is open & C2 is open & C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & (A1 \/ A2 c= C1 \/ C2 or ex C being non empty Subset of X st C is closed & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2) \/ C); theorem :: TSEP_1:65 A1 \/ A2 = the carrier of X implies (A1,A2 are_weakly_separated iff ex C1, C2, C being Subset of X st A1 \/ A2 = (C1 \/ C2) \/ C & C1 c= A1 & C2 c= A2 & C c= A1 /\ A2 & C1 is open & C2 is open & C is closed); theorem :: TSEP_1:66 A1 \/ A2 = the carrier of X & A1,A2 are_weakly_separated & not A1 c= A2 & not A2 c= A1 implies ex C1, C2 being non empty Subset of X st C1 is open & C2 is open & C1 c= A1 & C2 c= A2 & (A1 \/ A2 = C1 \/ C2 or ex C being non empty Subset of X st A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1 /\ A2 & C is closed); ::A Characterization of Separated Subsets by means of Weakly Separated ones. theorem :: TSEP_1:67 A1,A2 are_separated iff ex B1, B2 being Subset of X st B1,B2 are_weakly_separated & A1 c= B1 & A2 c= B2 & B1 /\ B2 misses A1 \/ A2; begin ::4. Separated and Weakly Separated Subspaces of Topological Spaces. reserve X for non empty TopSpace; definition let X be TopStruct; let X1, X2 be SubSpace of X; pred X1,X2 are_separated means :: TSEP_1:def 8 for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds A1,A2 are_separated; symmetry; antonym X1,X2 are_not_separated; end; reserve X1, X2 for non empty SubSpace of X; ::Properties of Separated Subspaces of Topological Spaces. theorem :: TSEP_1:68 X1,X2 are_separated implies X1 misses X2; canceled; theorem :: TSEP_1:70 for X1, X2 being closed non empty SubSpace of X holds X1 misses X2 iff X1,X2 are_separated; theorem :: TSEP_1:71 X = X1 union X2 & X1,X2 are_separated implies X1 is closed SubSpace of X; theorem :: TSEP_1:72 X1 union X2 is closed SubSpace of X & X1,X2 are_separated implies X1 is closed SubSpace of X; theorem :: TSEP_1:73 for X1, X2 being open non empty SubSpace of X holds X1 misses X2 iff X1,X2 are_separated; theorem :: TSEP_1:74 X = X1 union X2 & X1,X2 are_separated implies X1 is open SubSpace of X; theorem :: TSEP_1:75 X1 union X2 is open SubSpace of X & X1,X2 are_separated implies X1 is open SubSpace of X; ::Restriction Theorems for Separated Subspaces. theorem :: TSEP_1:76 for Y, X1, X2 being non empty SubSpace of X st X1 meets Y & X2 meets Y holds X1,X2 are_separated implies X1 meet Y,X2 meet Y are_separated & Y meet X1,Y meet X2 are_separated; theorem :: TSEP_1:77 for Y1, Y2 being SubSpace of X st Y1 is SubSpace of X1 & Y2 is SubSpace of X2 holds X1,X2 are_separated implies Y1,Y2 are_separated; theorem :: TSEP_1:78 for Y being non empty SubSpace of X st X1 meets X2 holds X1,Y are_separated implies X1 meet X2,Y are_separated; theorem :: TSEP_1:79 for Y being non empty SubSpace of X holds X1,Y are_separated & X2,Y are_separated iff X1 union X2,Y are_separated; theorem :: TSEP_1:80 X1,X2 are_separated iff ex Y1, Y2 being closed non empty SubSpace of X st X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & Y1 misses X2 & Y2 misses X1; ::First Characterization of Separated Subspaces of Topological Spaces. theorem :: TSEP_1:81 X1,X2 are_separated iff ex Y1, Y2 being closed non empty SubSpace of X st X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & (Y1 misses Y2 or Y1 meet Y2 misses X1 union X2); theorem :: TSEP_1:82 X1,X2 are_separated iff ex Y1, Y2 being open non empty SubSpace of X st X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & Y1 misses X2 & Y2 misses X1; ::Second Characterization of Separated Subspaces of Topological Spaces. theorem :: TSEP_1:83 X1,X2 are_separated iff ex Y1, Y2 being open non empty SubSpace of X st X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & (Y1 misses Y2 or Y1 meet Y2 misses X1 union X2); definition let X be TopStruct, X1, X2 be SubSpace of X; pred X1,X2 are_weakly_separated means :: TSEP_1:def 9 for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds A1,A2 are_weakly_separated; symmetry; antonym X1,X2 are_not_weakly_separated; end; reserve X1, X2 for non empty SubSpace of X; ::Properties of Weakly Separated Subspaces of Topological Spaces. canceled; theorem :: TSEP_1:85 X1 misses X2 & X1,X2 are_weakly_separated iff X1,X2 are_separated; theorem :: TSEP_1:86 X1 is SubSpace of X2 implies X1,X2 are_weakly_separated; theorem :: TSEP_1:87 for X1, X2 being closed SubSpace of X holds X1,X2 are_weakly_separated; theorem :: TSEP_1:88 for X1, X2 being open SubSpace of X holds X1,X2 are_weakly_separated; ::Extension Theorems for Weakly Separated Subspaces. theorem :: TSEP_1:89 for Y being non empty SubSpace of X holds X1,X2 are_weakly_separated implies X1 union Y,X2 union Y are_weakly_separated; theorem :: TSEP_1:90 for Y1, Y2 being non empty SubSpace of X st Y1 is SubSpace of X2 & Y2 is SubSpace of X1 holds X1,X2 are_weakly_separated implies X1 union Y1,X2 union Y2 are_weakly_separated & Y1 union X1,Y2 union X2 are_weakly_separated; theorem :: TSEP_1:91 for Y, X1, X2 being non empty SubSpace of X st X1 meets X2 holds (X1,Y are_weakly_separated & X2,Y are_weakly_separated implies X1 meet X2,Y are_weakly_separated) & (Y,X1 are_weakly_separated & Y,X2 are_weakly_separated implies Y,X1 meet X2 are_weakly_separated); theorem :: TSEP_1:92 for Y being non empty SubSpace of X holds (X1,Y are_weakly_separated & X2,Y are_weakly_separated implies X1 union X2,Y are_weakly_separated) & (Y,X1 are_weakly_separated & Y,X2 are_weakly_separated implies Y,X1 union X2 are_weakly_separated); ::First Characterization of Weakly Separated Subspaces of Topological Spaces. theorem :: TSEP_1:93 for X being non empty TopSpace, X1,X2 being non empty SubSpace of X holds X1 meets X2 implies (X1,X2 are_weakly_separated iff (X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1, Y2 being closed non empty SubSpace of X st Y1 meet (X1 union X2) is SubSpace of X1 & Y2 meet (X1 union X2) is SubSpace of X2 & (X1 union X2 is SubSpace of Y1 union Y2 or ex Y being open non empty SubSpace of X st the TopStruct of X = (Y1 union Y2) union Y & Y meet (X1 union X2) is SubSpace of X1 meet X2))); theorem :: TSEP_1:94 X = X1 union X2 & X1 meets X2 implies (X1,X2 are_weakly_separated iff (X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1, Y2 being closed non empty SubSpace of X st Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & (X = Y1 union Y2 or ex Y being open non empty SubSpace of X st X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2))); theorem :: TSEP_1:95 X = X1 union X2 & X1 misses X2 implies (X1,X2 are_weakly_separated iff X1 is closed SubSpace of X & X2 is closed SubSpace of X); ::Second Characterization of Weakly Separated Subspaces of Topological Spaces. theorem :: TSEP_1:96 for X being non empty TopSpace, X1,X2 being non empty SubSpace of X holds X1 meets X2 implies (X1,X2 are_weakly_separated iff (X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1, Y2 being open non empty SubSpace of X st Y1 meet (X1 union X2) is SubSpace of X1 & Y2 meet (X1 union X2) is SubSpace of X2 & (X1 union X2 is SubSpace of Y1 union Y2 or ex Y being closed non empty SubSpace of X st the TopStruct of X = (Y1 union Y2) union Y & Y meet (X1 union X2) is SubSpace of X1 meet X2))); theorem :: TSEP_1:97 X = X1 union X2 & X1 meets X2 implies (X1,X2 are_weakly_separated iff (X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1, Y2 being open non empty SubSpace of X st Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & (X = Y1 union Y2 or ex Y being closed non empty SubSpace of X st X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2))); theorem :: TSEP_1:98 X = X1 union X2 & X1 misses X2 implies (X1,X2 are_weakly_separated iff X1 is open SubSpace of X & X2 is open SubSpace of X); ::A Characterization of Separated Subspaces by means of Weakly Separated ones. theorem :: TSEP_1:99 X1,X2 are_separated iff ex Y1, Y2 being non empty SubSpace of X st Y1,Y2 are_weakly_separated & X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & (Y1 misses Y2 or Y1 meet Y2 misses X1 union X2);

Back to top