:: Introduction to Real Linear Topological Spaces :: by Czes{\l}aw Byli\'nski :: :: Received October 6, 2004 :: Copyright (c) 2004-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, REAL_1, XBOOLE_0, RLVECT_1, SUBSET_1, PRE_TOPC, RELAT_1, XCMPLX_0, SETFAM_1, TARSKI, ALGSTR_0, ARYTM_3, ZFMISC_1, STRUCT_0, SUPINF_2, ARYTM_1, CONNSP_2, TOPS_1, CONVEX1, CARD_1, XXREAL_0, RELAT_2, COMPLEX1, BINOP_1, FUNCT_1, RCOMP_1, ORDINAL2, TOPS_2, YELLOW13, XXREAL_2, FINSET_1, RVSUM_1, EQREL_1, COMPTS_1, RLTOPSP1, FUNCT_2, INCSP_1, AFF_1, PENCIL_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSET_1, SETFAM_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2, BINOP_1, REAL_1, EQREL_1, DOMAIN_1, STRUCT_0, ALGSTR_0, PRE_TOPC, TOPS_1, TOPS_2, CONNSP_2, COMPTS_1, YELLOW13, RLVECT_1, RUSUB_4, CONVEX1; constructors SETFAM_1, BINOP_1, DOMAIN_1, XXREAL_0, REAL_1, COMPLEX1, EQREL_1, TOPS_1, TOPS_2, CONNSP_2, RUSUB_4, CONVEX1, URYSOHN1, YELLOW13, COMPTS_1, RELSET_1, NUMBERS; registrations XBOOLE_0, SUBSET_1, RELSET_1, PARTFUN1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, STRUCT_0, TOPS_1, RLVECT_1, CONVEX1, TOPGRP_1, ORDINAL1, BORSUK_1, COMPTS_1, PRE_TOPC, FUNCT_2, ANPROJ_1; requirements BOOLE, REAL, NUMERALS, SUBSET, ARITHM; definitions TARSKI, XBOOLE_0, STRUCT_0, RLVECT_1, PRE_TOPC, CONNSP_2, TOPS_2, YELLOW13, CONVEX1, ALGSTR_0, SETFAM_1, ZFMISC_1; equalities STRUCT_0, RLVECT_1, CONVEX1, SUBSET_1, ALGSTR_0, XCMPLX_0; expansions TARSKI, XBOOLE_0, PRE_TOPC, TOPS_2, CONVEX1; theorems TARSKI, XBOOLE_0, XBOOLE_1, ZFMISC_1, SUBSET_1, SETFAM_1, XCMPLX_1, XREAL_0, XCMPLX_0, FUNCT_2, FUNCT_1, ABSVALUE, FINSET_1, EQREL_1, PRE_TOPC, COMPTS_1, CONNSP_2, TOPS_1, URYSOHN1, YELLOW13, RLVECT_1, RUSUB_4, CONVEX1, TOPGRP_1, TOPS_2, YELLOW_8, XREAL_1, TSEP_1, COMPLEX1, XXREAL_0, XTUPLE_0, STRUCT_0; schemes BINOP_1, FUNCT_2, SUBSET_1, EQREL_1, FINSET_1; begin :: Preliminaries reserve r,s,t,u for Real; theorem for X being non empty RLSStruct, M being Subset of X, x being Point of X, r being Real st x in M holds r*x in r*M; reconsider jj=1 as positive Real; registration cluster non zero for Real; existence proof take jj; thus thesis; end; end; theorem Th2: for T being non empty TopSpace, X being non empty Subset of T, FX being Subset-Family of T st FX is Cover of X for x being Point of T st x in X ex W being Subset of T st x in W & W in FX proof let T be non empty TopSpace, X be non empty Subset of T, FX be Subset-Family of T; assume FX is Cover of X; then A1: X c= union FX by SETFAM_1:def 11; let x be Point of T; assume x in X; then consider W being set such that A2: x in W and A3: W in FX by A1,TARSKI:def 4; reconsider W as Subset of T by A3; take W; thus thesis by A2,A3; end; theorem Th3: for X being non empty addLoopStr, M,N being Subset of X, x,y being Point of X st x in M & y in N holds x+y in M+N proof let X be non empty addLoopStr, M,N be Subset of X, x,y be Point of X; M+N = {u + v where u,v is Point of X: u in M & v in N} by RUSUB_4:def 9; hence thesis; end; Lm1: for X being non empty addLoopStr, M being Subset of X, x,y being Point of X st y in M holds x+y in x+M proof let X be non empty addLoopStr, M be Subset of X, x,y be Point of X; x+M = {x + u where u is Point of X: u in M} by RUSUB_4:def 8; hence thesis; end; Lm2: for X being non empty addLoopStr, M,N being Subset of X holds {x+N where x is Point of X: x in M} is Subset-Family of X proof let X be non empty addLoopStr, M,N be Subset of X; set F = {u+N where u is Point of X: u in M}; F c= bool the carrier of X proof let x be object; assume x in F; then ex u being Point of X st x=u+N & u in M; hence thesis; end; hence thesis; end; theorem Th4: for X being non empty addLoopStr, M,N being Subset of X, F being Subset-Family of X st F = {x+N where x is Point of X: x in M} holds M+N = union F proof let X be non empty addLoopStr, M,N be Subset of X, F be Subset-Family of X; assume A1: F = {x+N where x is Point of X: x in M}; thus M+N c= union F proof let x be object; assume x in M+N; then x in {u+v where u,v is Point of X: u in M & v in N} by RUSUB_4:def 9; then consider u,v being Point of X such that A2: x = u+v and A3: u in M and A4: v in N; u+N = {u + v9 where v9 is Point of X: v9 in N} by RUSUB_4:def 8; then A5: x in u+N by A2,A4; u+N in F by A1,A3; hence thesis by A5,TARSKI:def 4; end; let x be object; assume x in union F; then consider Y being set such that A6: x in Y and A7: Y in F by TARSKI:def 4; consider u being Point of X such that A8: Y = u+N and A9: u in M by A1,A7; u+N = {u + v where v is Point of X: v in N} by RUSUB_4:def 8; then ex v being Point of X st x = u+v & v in N by A6,A8; then x in {u9+v9 where u9,v9 is Point of X: u9 in M & v9 in N} by A9; hence thesis by RUSUB_4:def 9; end; theorem Th5: for X being add-associative right_zeroed right_complementable non empty addLoopStr, M being Subset of X holds 0.X+M = M proof let X be add-associative right_zeroed right_complementable non empty addLoopStr, M be Subset of X; A1: 0.X+M = {0.X + u where u is Point of X: u in M} by RUSUB_4:def 8; thus 0.X+M c= M proof let x be object; assume x in 0.X+M; then ex u being Point of X st x = 0.X+u & u in M by A1; hence thesis; end; let x be object; assume A2: x in M; then reconsider x as Point of X; 0.X+x = x; hence thesis by A1,A2; end; theorem Th6: for X being add-associative non empty addLoopStr,x,y being Point of X, M being Subset of X holds x+y+M = x+(y+M) proof let X be add-associative non empty addLoopStr,x,y be Point of X, M be Subset of X; A1: x+(y+M) = {x+u where u is Point of X: u in y+M} by RUSUB_4:def 8; A2: y+M = {y+u where u is Point of X: u in M} by RUSUB_4:def 8; A3: x+y+M = {x+y+u where u is Point of X: u in M} by RUSUB_4:def 8; thus x+y+M c= x+(y+M) proof let z be object; assume z in x+y+M; then consider u being Point of X such that A4: x+y+u = z & u in M by A3; x+(y+u) = z & y+u in y+M by A2,A4,RLVECT_1:def 3; hence thesis by A1; end; let z be object; assume z in x+(y+M); then consider u being Point of X such that A5: x+u = z and A6: u in y+M by A1; consider v being Point of X such that A7: y+v = u and A8: v in M by A2,A6; x+y+v = z by A5,A7,RLVECT_1:def 3; hence thesis by A3,A8; end; theorem Th7: for X being add-associative non empty addLoopStr, x being Point of X, M,N being Subset of X holds x+M+N = x+(M+N) proof let X be add-associative non empty addLoopStr, x be Point of X, M,N be Subset of X; A1: x+(M+N) = {x+u where u is Point of X: u in M+N} by RUSUB_4:def 8; A2: x+M = {x+u where u is Point of X: u in M} by RUSUB_4:def 8; A3: M+N = {u+v where u,v is Point of X: u in M & v in N} by RUSUB_4:def 9; A4: x+M+N = {u+v where u,v is Point of X: u in x+M & v in N} by RUSUB_4:def 9; thus x+M+N c= x+(M+N) proof let z be object; assume z in x+M+N; then consider u,v being Point of X such that A5: u+v = z and A6: u in x+M and A7: v in N by A4; consider u9 being Point of X such that A8: x+u9 = u & u9 in M by A2,A6; x+(u9+v) = z & u9+v in M+N by A3,A5,A7,A8,RLVECT_1:def 3; hence thesis by A1; end; let z be object; assume z in x+(M+N); then consider u being Point of X such that A9: x+u = z and A10: u in M+N by A1; consider w,v being Point of X such that A11: w+v = u and A12: w in M and A13: v in N by A3,A10; A14: x+w in x+M by A2,A12; x+w+v = z by A9,A11,RLVECT_1:def 3; hence thesis by A4,A13,A14; end; theorem Th8: for X being non empty addLoopStr, M,N being Subset of X, x being Point of X st M c= N holds x+M c= x+N proof let X be non empty addLoopStr, M,N be Subset of X, x be Point of X such that A1: M c= N; let z be object; assume A2: z in x+M; then reconsider z as Point of X; x+M = {x + u where u is Element of X: u in M} by RUSUB_4:def 8; then ex u being Point of X st x+u = z & u in M by A2; hence thesis by A1,Lm1; end; theorem Th9: for X being add-associative right_zeroed right_complementable non empty addLoopStr, M being Subset of X, x being Point of X st x in M holds 0.X in -x+M proof let X be add-associative right_zeroed right_complementable non empty addLoopStr, M be Subset of X, x be Point of X; assume x in M; then -x+x in -x+M by Lm1; hence thesis by RLVECT_1:5; end; theorem Th10: for X being non empty addLoopStr, M,N,V being Subset of X st M c= N holds M+V c= N+V proof let X be non empty addLoopStr, M,N,V be Subset of X such that A1: M c= N; let x be object; assume x in M+V; then x in {u + v where u,v is Point of X: u in M & v in V} by RUSUB_4:def 9; then ex u,v being Point of X st u+v = x & u in M & v in V; then x in {u9 + v9 where u9,v9 is Point of X: u9 in N & v9 in V} by A1; hence thesis by RUSUB_4:def 9; end; Lm3: for X being non empty addLoopStr, M,N,V being Subset of X st M c= N holds V+M c= V+N proof let X be non empty addLoopStr, M,N,V be Subset of X such that A1: M c= N; let x be object; assume x in V+M; then x in {u + v where u,v is Point of X: u in V & v in M} by RUSUB_4:def 9; then ex u,v being Point of X st u+v = x & u in V & v in M; then x in {u9 + v9 where u9,v9 is Point of X: u9 in V & v9 in N} by A1; hence thesis by RUSUB_4:def 9; end; theorem Th11: for X being non empty addLoopStr, V1,V2,W1,W2 being Subset of X st V1 c= W1 & V2 c= W2 holds V1+V2 c= W1+W2 proof let X be non empty addLoopStr, V1,V2,W1,W2 be Subset of X such that A1: V1 c= W1 & V2 c= W2; let x be object; assume x in V1+V2; then x in {u + v where u,v is Point of X: u in V1 & v in V2} by RUSUB_4:def 9 ; then ex u,v being Point of X st u+v = x & u in V1 & v in V2; then x in {u9 + v9 where u9,v9 is Point of X: u9 in W1 & v9 in W2} by A1; hence thesis by RUSUB_4:def 9; end; theorem Th12: for X being right_zeroed non empty addLoopStr, V1,V2 being Subset of X st 0.X in V2 holds V1 c= V1+V2 proof let X be right_zeroed non empty addLoopStr, V1,V2 be Subset of X such that A1: 0.X in V2; let x be object; assume A2: x in V1; then reconsider x as Point of X; x+0.X = x by RLVECT_1:def 4; then x in {u + v where u,v is Point of X: u in V1 & v in V2} by A1,A2; hence thesis by RUSUB_4:def 9; end; theorem Th13: for X being RealLinearSpace, r being Real holds r*{0.X} = {0.X} proof let X be RealLinearSpace, r be Real; thus r*{0.X} c= {0.X} proof let x be object; assume A1: x in r*{0.X}; then reconsider x as Point of X; consider v being Point of X such that A2: x = r*v and A3: v in {0.X} by A1; v = 0.X by A3,TARSKI:def 1; then r*v = 0.X; hence thesis by A2,TARSKI:def 1; end; 0.X in {0.X} by TARSKI:def 1; then r*0.X in r*{0.X}; then 0.X in r*{0.X}; hence thesis by ZFMISC_1:31; end; theorem for X being RealLinearSpace, M being Subset of X, r being non zero Real st 0.X in r*M holds 0.X in M proof let X be RealLinearSpace, M be Subset of X, r be non zero Real; assume 0.X in r*M; then A1: ex v being Point of X st r*v = 0.X & v in M; r * 0.X = 0.X; hence thesis by A1,RLVECT_1:36; end; theorem Th15: for X being RealLinearSpace, M,N being Subset of X, r being non zero Real holds (r * M) /\ (r * N) = r * (M /\ N) proof let X be RealLinearSpace, M,N be Subset of X, r be non zero Real; thus for x being object st x in (r * M) /\ (r * N) holds x in r * (M /\ N) proof let x be object; assume A1: x in (r * M) /\ (r * N); then x in r * M by XBOOLE_0:def 4; then consider v1 being Point of X such that A2: r*v1 = x and A3: v1 in M; x in (r * N) by A1,XBOOLE_0:def 4; then consider v2 being Point of X such that A4: r*v2 = x and A5: v2 in N; v1 = v2 by A2,A4,RLVECT_1:36; then v1 in M /\ N by A3,A5,XBOOLE_0:def 4; hence thesis by A2; end; let x be object; assume x in r * (M /\ N); then consider v being Point of X such that A6: r*v = x and A7: v in M /\ N; v in N by A7,XBOOLE_0:def 4; then A8: x in r*N by A6; v in M by A7,XBOOLE_0:def 4; then x in r*M by A6; hence thesis by A8,XBOOLE_0:def 4; end; theorem for X being non empty TopSpace, x being Point of X, A being a_neighborhood of x, B being Subset of X st A c= B holds B is a_neighborhood of x proof let X be non empty TopSpace, x be Point of X, A be a_neighborhood of x, B be Subset of X; assume A c= B; then x in Int A & Int A c= Int B by CONNSP_2:def 1,TOPS_1:19; hence thesis by CONNSP_2:def 1; end; definition let V be RealLinearSpace, M be Subset of V; redefine attr M is convex means :Def1: for u,v being Point of V, r being Real st 0 <= r & r <= 1 & u in M & v in M holds r*u + (1-r)*v in M; compatibility proof hereby assume A1: M is convex; let u,v be Point of V, r be Real such that A2: 0 <= r & r <= 1 and A3: u in M and A4: v in M; per cases by A2,XXREAL_0:1; suppose 0 < r & r < 1; hence r*u + (1-r)*v in M by A1,A3,A4; end; suppose 0 = r; then r*u = 0.V & (1-r)*v = v by RLVECT_1:10,def 8; hence r*u + (1-r)*v in M by A4; end; suppose r = 1; then (1-r)*v = 0.V & r*u = u by RLVECT_1:10,def 8; hence r*u + (1-r)*v in M by A3; end; end; assume A5: for u,v being Point of V, r being Real st 0 <= r & r <= 1 & u in M & v in M holds r*u + (1-r)*v in M; let u,v be Point of V, r be Real; thus thesis by A5; end; end; Lm4: for X being RealLinearSpace holds conv({}X) = {} proof let X be RealLinearSpace; {}X is convex; then {}X in Convex-Family {}X by CONVEX1:def 4; hence thesis by SETFAM_1:4; end; registration let X be RealLinearSpace, M be empty Subset of X; cluster conv(M) -> empty; coherence proof M = {}X; hence thesis by Lm4; end; end; theorem for X being RealLinearSpace, M being convex Subset of X holds conv(M) = M by CONVEX1:30,CONVEX1:41; theorem Th18: for X being RealLinearSpace, M being Subset of X, r being Real holds r*conv(M) = conv(r*M) proof let X be RealLinearSpace, M be Subset of X, r be Real; thus r*conv(M) c= conv(r*M) proof let x be object; per cases; suppose A1: r = 0; per cases; suppose M = {}; hence thesis by CONVEX1:33; end; suppose A2: M <> {}; then r*M = {0.X} by A1,CONVEX1:34; then A3: {0.X} c= conv(r*M) by CONVEX1:41; conv(M) <> {} by A2,CONVEX1:41,XBOOLE_1:3; then r*conv(M) = {0.X} by A1,CONVEX1:34; hence thesis by A3; end; end; suppose A4: r <> 0; assume x in r*conv(M); then consider v being Point of X such that A5: x = r*v and A6: v in conv(M); for V being set st V in Convex-Family(r*M) holds r*v in V proof let V be set; assume A7: V in Convex-Family(r*M); then reconsider V as Subset of X; r*M c= V by A7,CONVEX1:def 4; then r"*(r*M) c= r"*V by CONVEX1:39; then (r"*r)*M c= r"*V by CONVEX1:37; then 1*M c= r"*V by A4,XCMPLX_0:def 7; then A8: M c= r"*V by CONVEX1:32; V is convex by A7,CONVEX1:def 4; then r"*V is convex by CONVEX1:1; then r"*V in Convex-Family M by A8,CONVEX1:def 4; then v in r"*V by A6,SETFAM_1:def 1; then consider w being Point of X such that A9: v = r"*w and A10: w in V; r*v = (r*r")*w by A9,RLVECT_1:def 7 .= 1*w by A4,XCMPLX_0:def 7 .= w by RLVECT_1:def 8; hence thesis by A10; end; hence thesis by A5,SETFAM_1:def 1; end; end; r*M c= r*conv(M) & r*conv(M) is convex by CONVEX1:1,39,41; hence thesis by CONVEX1:30; end; theorem Th19: for X being RealLinearSpace, M1,M2 being Subset of X st M1 c= M2 holds Convex-Family M2 c= Convex-Family M1 proof let X be RealLinearSpace, M1,M2 be Subset of X such that A1: M1 c= M2; let M be object; assume A2: M in Convex-Family M2; then reconsider M as Subset of X; M2 c= M by A2,CONVEX1:def 4; then A3: M1 c= M by A1; M is convex by A2,CONVEX1:def 4; hence thesis by A3,CONVEX1:def 4; end; theorem Th20: for X being RealLinearSpace, M1,M2 being Subset of X st M1 c= M2 holds conv(M1) c= conv(M2) proof let X be RealLinearSpace, M1,M2 be Subset of X; assume M1 c= M2; then Convex-Family M2 c= Convex-Family M1 by Th19; then A1: meet (Convex-Family M1) c= meet (Convex-Family M2) by SETFAM_1:6; let x be object; assume x in conv(M1); hence thesis by A1; end; theorem for X being RealLinearSpace, M being convex Subset of X, r being Real st 0 <= r & r <= 1 & 0.X in M holds r*M c= M proof let X be RealLinearSpace, M be convex Subset of X, r be Real such that A1: 0 <= r & r <= 1 & 0.X in M; let x be object; assume x in r*M; then consider v being Point of X such that A2: r*v = x and A3: v in M; r*v + (1-r)*0.X in M by A1,A3,Def1; then r*v + 0.X in M; hence thesis by A2; end; definition let X be RealLinearSpace, v,w be Point of X; func LSeg(v,w) -> Subset of X equals {(1-r)*v + r*w : 0 <= r & r <= 1 }; coherence proof {(1-r)*v + r*w: 0 <= r & r <= 1 } c= the carrier of X proof let x be object; assume x in {(1-r)*v + r*w: 0 <= r & r <= 1 }; then ex r st x = (1-r)*v + r*w & 0 <= r & r <= 1; hence thesis; end; hence thesis; end; commutativity proof let A be Subset of X, v,w be Point of X; assume A1: A = {(1-r)*v + r*w : 0 <= r & r <= 1 }; thus A c= {(1-r)*w + r*v : 0 <= r & r <= 1 } proof let x be object; assume x in A; then consider r such that A2: x = (1-r)*v + r*w and A3: 0 <= r & r <= 1 by A1; A4: 1-(1-r)=r; 0 <= 1-r & 1-r <= 1-0 by A3,XREAL_1:10,48; hence thesis by A2,A4; end; let x be object; assume x in {(1-r)*w + r*v : 0 <= r & r <= 1 }; then consider r such that A5: x = (1-r)*w + r*v and A6: 0 <= r & r <= 1; A7: 1-(1-r)=r; 0 <= 1-r & 1-r <= 1-0 by A6,XREAL_1:10,48; hence thesis by A1,A5,A7; end; end; registration let X be RealLinearSpace, v,w be Point of X; cluster LSeg(v,w) -> non empty convex; coherence proof A1: 0 * w = 0.X & v + 0.X = v by RLVECT_1:10; 1 - 0 = 1 & 1 * v = v by RLVECT_1:def 8; then v in LSeg(v,w) by A1; hence LSeg(v,w) is non empty; let u,u9 be Point of X, r be Real; assume that A2: 0 <= r and A3: r <= 1; A4: 0 <= 1-r by A3,XREAL_1:48; assume u in LSeg(v,w); then consider s being Real such that A5: u = (1-s)*v + s*w and A6: 0 <= s and A7: s <= 1; A8: r*u = r*((1-s)*v) + r*(s*w) by A5,RLVECT_1:def 5 .= r*(1-s)*v + r*(s*w) by RLVECT_1:def 7 .= r*(1-s)*v + r*s*w by RLVECT_1:def 7; assume u9 in LSeg(v,w); then consider t being Real such that A9: u9 = (1-t)*v + t*w and A10: 0 <= t and A11: t <= 1; (1-r)*u9 = (1-r)*((1-t)*v) + (1-r)*(t*w) by A9,RLVECT_1:def 5 .= (1-r)*(1-t)*v + (1-r)*(t*w) by RLVECT_1:def 7 .= (1-r)*(1-t)*v + (1-r)*t*w by RLVECT_1:def 7; then A12: r*u + (1-r)*u9 = r*(1-s)*v + (r*s*w + ((1-r)*(1-t)*v + (1-r)*t*w)) by A8, RLVECT_1:def 3 .= r*(1-s)*v + ((1-r)*(1-t)*v + (r*s*w + (1-r)*t*w)) by RLVECT_1:def 3 .= r*(1-s)*v + (1-r)*(1-t)*v + (r*s*w + (1-r)*t*w) by RLVECT_1:def 3 .= (r*(1-s) + (1-r)*(1-t))*v + (r*s*w + (1-r)*t*w) by RLVECT_1:def 6 .= (1 - ((r*s + (1-r)*t)))*v + (r*s + (1-r)*t)*w by RLVECT_1:def 6; (1-r)*t + r*s <= 1 by A2,A3,A7,A11,XREAL_1:174; hence thesis by A2,A6,A10,A12,A4; end; end; theorem for X being RealLinearSpace, M being Subset of X holds M is convex iff for u,w being Point of X st u in M & w in M holds LSeg(u,w) c= M proof let X be RealLinearSpace, M be Subset of X; hereby assume A1: M is convex; let u,w be Point of X such that A2: u in M & w in M; thus LSeg(u,w) c= M proof let x be object; assume x in LSeg(u,w); then ex r st x = (1-r)*u + r*w & 0 <= r & r <= 1; hence x in M by A1,A2; end; end; assume A3: for w,u being Point of X st w in M & u in M holds LSeg(w,u) c= M; let u,w be Point of X, r be Real such that A4: 0 <= r & r <= 1 and A5: u in M & w in M; A6: r*u + (1-r)*w in LSeg(w,u) by A4; LSeg(w,u) c= M by A3,A5; hence thesis by A6; end; definition let V be non empty RLSStruct, P be Subset-Family of V; attr P is convex-membered means :Def3: for M being Subset of V st M in P holds M is convex; end; registration let V be non empty RLSStruct; cluster non empty convex-membered for Subset-Family of V; existence proof reconsider F = {{}V} as Subset-Family of V; take F; thus F is non empty; let M be Subset of V; assume M in F; then M = {}V by TARSKI:def 1; hence thesis; end; end; theorem for V being non empty RLSStruct, F being convex-membered Subset-Family of V holds meet F is convex proof let V be non empty RLSStruct, F be convex-membered Subset-Family of V; for M being Subset of V st M in F holds M is convex by Def3; hence thesis by CONVEX1:15; end; definition let X be non empty RLSStruct, A be Subset of X; func -A -> Subset of X equals (-1)*A; coherence; end; theorem Th24: for X being RealLinearSpace, M,N being Subset of X, v being Point of X holds v+M meets N iff v in N+(-M) proof let X be RealLinearSpace, M,N be Subset of X, v being Point of X; A1: N+(-1)*M = {u + w where u,w is Point of X: u in N & w in (-1)*M} by RUSUB_4:def 9; hereby A2: v+M = {v + u where u is Point of X: u in M} by RUSUB_4:def 8; assume v+M meets N; then consider z being object such that A3: z in v+M and A4: z in N by XBOOLE_0:3; consider u being Point of X such that A5: v+u = z and A6: u in M by A3,A2; reconsider z as Point of X by A3; A7: (-1)*u in (-1)*M by A6; z + (-1)*u = v + (u + (-1)*u) by A5,RLVECT_1:def 3 .= v + (u + -u) by RLVECT_1:16 .= v+ 0.X by RLVECT_1:5 .= v; hence v in N+-M by A4,A7,Th3; end; assume v in N+(-M); then consider u,w being Point of X such that A8: v = u+w and A9: u in N and A10: w in (-1)*M by A1; consider w9 being Point of X such that A11: w = (-1)*w9 and A12: w9 in M by A10; A13: (-1)*w = (-1)*(-1)*w9 by A11,RLVECT_1:def 7 .= w9 by RLVECT_1:def 8; v+w9 = u + (w+w9) by A8,RLVECT_1:def 3 .= u + (w+-w) by A13,RLVECT_1:16 .= u + 0.X by RLVECT_1:5 .= u; then u in v+M by A12,Lm1; hence thesis by A9,XBOOLE_0:3; end; definition let X be non empty RLSStruct, A be Subset of X; attr A is symmetric means :Def5: A = -A; end; registration let X be RealLinearSpace; cluster non empty symmetric for Subset of X; existence proof take V = {0.X}; thus V is non empty; thus V = -V by Th13; end; end; theorem Th25: for X being RealLinearSpace, A being symmetric Subset of X, x being Point of X st x in A holds -x in A proof let X be RealLinearSpace, A be symmetric Subset of X, x be Point of X such that A1: x in A; A = -A by Def5 .= (-1)*A; then consider v being Point of X such that A2: x = (-1)*v and A3: v in A by A1; (-1)*x = (-1)*(-1)*v by A2,RLVECT_1:def 7 .= v by RLVECT_1:def 8; hence thesis by A3,RLVECT_1:16; end; definition let X be non empty RLSStruct, A be Subset of X; attr A is circled means :Def6: for r being Real st |.r.| <= 1 holds r*A c= A; end; registration let X be non empty RLSStruct; cluster empty -> circled for Subset of X; coherence by CONVEX1:33; end; theorem Th26: for X being RealLinearSpace holds {0.X} is circled by Th13; registration let X be RealLinearSpace; cluster non empty circled for Subset of X; existence proof take {0.X}; thus thesis by Th26; end; end; theorem Th27: for X being RealLinearSpace, B being non empty circled Subset of X holds 0.X in B proof let X be RealLinearSpace; let B be non empty circled Subset of X; |. 0 .| = 0 by ABSVALUE:2; then 0*B c= B by Def6; then A1: {0.X} c= B by CONVEX1:34; 0.X in {0.X} by TARSKI:def 1; hence thesis by A1; end; Lm5: for X being RealLinearSpace,A,B being circled Subset of X holds A+B is circled proof let X be non empty RealLinearSpace,A,B be circled Subset of X; A1: A+B = {u + v where u,v is Point of X: u in A & v in B} by RUSUB_4:def 9; let r be Real; assume |.r.| <= 1; then A2: r*A c= A & r*B c= B by Def6; let x be object; assume x in r*(A+B); then consider x9 being Point of X such that A3: x = r*x9 and A4: x9 in A+B; consider u,v being Point of X such that A5: x9 = u+v and A6: u in A & v in B by A1,A4; A7: r*u in r*A & r*v in r*B by A6; x = r*u+r*v by A3,A5,RLVECT_1:def 5; hence thesis by A2,A7,Th3; end; registration let X be RealLinearSpace, A,B be circled Subset of X; cluster A+B -> circled; coherence by Lm5; end; theorem Th28: for X being RealLinearSpace, A being circled Subset of X for r being Real st |.r.| = 1 holds r*A = A proof let X be RealLinearSpace, A be circled Subset of X; let r be Real; assume A1: |.r.| = 1; hence A2: r*A c= A by Def6; let x be object; assume A3: x in A; then reconsider x as Point of X; A4: r*x in r*A by A3; per cases; suppose 0 <= r; then r = 1 by A1,ABSVALUE:def 1; hence thesis by A3,CONVEX1:32; end; suppose r < 0; then |.r.| = -r by ABSVALUE:def 1; then (-1)*((-1)*x) in r*A by A1,A2,A4; then (-1)*(-1)*x in r*A by RLVECT_1:def 7; hence thesis by RLVECT_1:def 8; end; end; Lm6: for X being RealLinearSpace, A being circled Subset of X holds A is symmetric proof let X be RealLinearSpace, A be circled Subset of X; |.-1.| = --1 by ABSVALUE:def 1 .= 1; hence A = -A by Th28; end; registration let X be RealLinearSpace; cluster circled -> symmetric for Subset of X; coherence by Lm6; end; Lm7: for X being RealLinearSpace, M being circled Subset of X holds conv(M) is circled proof let X be RealLinearSpace, M be circled Subset of X; let r be Real; assume |.r.| <= 1; then A1: r*M c= M by Def6; r*conv(M) = conv(r*M) by Th18; hence thesis by A1,Th20; end; registration let X be RealLinearSpace, M be circled Subset of X; cluster conv(M) -> circled; coherence by Lm7; end; definition let X be non empty RLSStruct, F be Subset-Family of X; attr F is circled-membered means :Def7: for V being Subset of X st V in F holds V is circled; end; registration let V be non empty RLSStruct; cluster non empty circled-membered for Subset-Family of V; existence proof reconsider F = {{}V} as Subset-Family of V; take F; thus F is non empty; let M be Subset of V; assume M in F; hence thesis by TARSKI:def 1; end; end; theorem for X being non empty RLSStruct, F being circled-membered Subset-Family of X holds union F is circled proof let X be non empty RLSStruct, F be circled-membered Subset-Family of X; let r be Real such that A1: |.r.| <= 1; let x be object; assume x in r*(union F); then consider x9 being Point of X such that A2: x = r*x9 and A3: x9 in union F; consider Y being set such that A4: x9 in Y and A5: Y in F by A3,TARSKI:def 4; reconsider Y as Subset of X by A5; Y is circled by A5,Def7; then A6: r*Y c= Y by A1; r*x9 in r*Y by A4; hence thesis by A2,A5,A6,TARSKI:def 4; end; theorem for X being non empty RLSStruct, F being circled-membered Subset-Family of X holds meet F is circled proof let X be non empty RLSStruct, F be circled-membered Subset-Family of X; let r be Real such that A1: |.r.| <= 1; let x be object; assume x in r*(meet F); then consider x9 being Point of X such that A2: x = r*x9 and A3: x9 in meet F; A4: now let Y be set; assume A5: Y in F; then reconsider Y9 = Y as Subset of X; x9 in Y by A3,A5,SETFAM_1:def 1; then A6: r*x9 in r*Y9; Y9 is circled by A5,Def7; then r*Y9 c= Y9 by A1; hence x in Y by A2,A6; end; F <> {} by A3,SETFAM_1:def 1; hence thesis by A4,SETFAM_1:def 1; end; begin definition struct(RLSStruct,TopStruct) RLTopStruct (# carrier -> set, ZeroF -> Element of the carrier, addF -> BinOp of the carrier, Mult -> Function of [:REAL, the carrier:],the carrier, topology -> Subset-Family of the carrier #); end; registration let X be non empty set, O be Element of X, F be BinOp of X, G be Function of [:REAL,X:],X, T be Subset-Family of X; cluster RLTopStruct (# X,O,F,G,T #) -> non empty; coherence; end; registration cluster strict non empty for RLTopStruct; existence proof set X = {0}; reconsider O = 0 as Element of X by TARSKI:def 1; set F = the BinOp of X; set G = the Function of [:REAL,X:],X; take RT = RLTopStruct (# X,O,F,G,{}bool X#); thus RT is strict; thus the carrier of RT is non empty; end; end; definition let X be non empty RLTopStruct; attr X is add-continuous means :Def8: for x1,x2 being Point of X, V being Subset of X st V is open & x1+x2 in V ex V1,V2 being Subset of X st V1 is open & V2 is open & x1 in V1 & x2 in V2 & V1+V2 c= V; attr X is Mult-continuous means :Def9: for a being Real, x being Point of X, V being Subset of X st V is open & a*x in V ex r being positive Real, W being Subset of X st W is open & x in W & for s being Real st |.s-a.| < r holds s*W c= V; end; registration cluster strict add-continuous Mult-continuous TopSpace-like Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital for non empty RLTopStruct; existence proof set ZS = {0}; set T = {{},ZS}; T c= bool ZS proof let x be object; reconsider xx=x as set by TARSKI:1; assume x in T; then x = {} or x = ZS by TARSKI:def 2; then xx c= ZS; hence thesis; end; then reconsider T as Subset-Family of ZS; reconsider O = 0 as Element of ZS by TARSKI:def 1; deffunc A((Element of ZS), Element of ZS) = O; consider F being BinOp of ZS such that A1: for x,y being Element of ZS holds F.(x,y) = A(x,y) from BINOP_1: sch 4; deffunc M(Real, Element of ZS) = O; consider G being Function of [:REAL,ZS:],ZS such that A2: for a being Element of REAL for x being Element of ZS holds G.(a,x ) = M(a,x) from BINOP_1:sch 4; take W = RLTopStruct (# ZS,O,F,G,T #); thus W is strict; thus W is add-continuous proof reconsider V1 = {O}, V2 = {O} as Subset of W; let x1,x2 be Point of W, V be Subset of W such that A3: V is open and A4: x1+x2 in V; take V1,V2; V1 in T by TARSKI:def 2; hence V1 is open & V2 is open; thus x1 in V1 & x2 in V2; V in T by A3; then V = the carrier of W by A4,TARSKI:def 2; hence thesis; end; thus W is Mult-continuous proof reconsider V9 = {O} as Subset of W; let a be Real, x be Point of W, V be Subset of W such that A5: V is open and A6: a*x in V; take jj,V9; V9 in T by TARSKI:def 2; hence V9 is open; thus x in V9; let s be Real such that |.s-a.| < jj; V in T by A5; then V = {} or V = ZS by TARSKI:def 2; hence thesis by A6; end; thus W is TopSpace-like proof thus the carrier of W in the topology of W by TARSKI:def 2; hereby let a be Subset-Family of W; assume a c= the topology of W; then a={} or a={{}} or a={ZS} or a={{},ZS} by ZFMISC_1:36; then union a={} or union a=ZS or union a = {} \/ ZS by ZFMISC_1:2,25,75 ; hence union a in the topology of W by TARSKI:def 2; end; let a,b be Subset of W such that A7: a in the topology of W and A8: b in the topology of W; A9: b={} or b=ZS by A8,TARSKI:def 2; a={} or a=ZS by A7,TARSKI:def 2; hence thesis by A9,TARSKI:def 2; end; thus for x,y being Point of W holds x + y = y + x proof let x,y be Point of W; reconsider X = x, Y = y as Element of ZS; x + y = A(X,Y) by A1; hence thesis by A1; end; thus for x,y,z being Point of W holds (x + y) + z = x + (y + z) proof let x,y,z be Point of W; reconsider X = x, Y = y, Z = z as Element of ZS; (x + y) + z = A(A(X,Y),Z) by A1; hence thesis by A1; end; thus for x being Point of W holds x + 0.W = x proof let x be Point of W; reconsider X = x as Element of ZS; x + 0.W = A(X,O) by A1; hence thesis by TARSKI:def 1; end; thus for x being Point of W holds x is right_complementable proof reconsider y = O as Point of W; let x be Point of W; take y; thus thesis by A1; end; thus for a being Real, x,y being Point of W holds a * (x + y) = a * x + a * y proof let a be Real; reconsider a as Element of REAL by XREAL_0:def 1; let x,y be Point of W; reconsider X = x, Y = y as Element of ZS; a * x + a * y = M(a,A(X,Y)) by A1 .= G.(a,A(X,Y)) by A2 .= G.(a,F.(x,y)) by A1; hence thesis; end; thus for a,b being Real for x being Point of W holds (a + b) * x = a * x + b * x proof let a,b be Real, x be Point of W; reconsider a,b as Element of REAL by XREAL_0:def 1; set c = a + b; reconsider X = x as Element of ZS; c * x = M(c,X) by A2; hence thesis by A1; end; thus for a,b being Real, x being Point of W holds (a * b) * x = a * (b * x) proof let a,b be Real, x be Point of W; reconsider a,b as Element of REAL by XREAL_0:def 1; set c = a * b; reconsider X = x as Element of ZS; c * x = M(c,X) by A2; hence thesis by A2; end; thus for x being Point of W holds 1 * x = x proof reconsider A9 = 1 as Element of REAL by XREAL_0:def 1 ; let x be Point of W; reconsider X = x as Element of ZS; A9 * x = M(A9,X) by A2; hence thesis by TARSKI:def 1; end; end; end; definition mode LinearTopSpace is add-continuous Mult-continuous TopSpace-like Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLTopStruct; end; theorem Th31: for X being LinearTopSpace, x1,x2 being Point of X, V being a_neighborhood of x1+x2 ex V1 being a_neighborhood of x1, V2 being a_neighborhood of x2 st V1+V2 c= V proof let X be LinearTopSpace; let x1,x2 be Point of X, V be a_neighborhood of x1+x2; x1+x2 in Int V by CONNSP_2:def 1; then consider V1,V2 being Subset of X such that A1: V1 is open and A2: V2 is open and A3: x1 in V1 and A4: x2 in V2 and A5: V1+V2 c= Int V by Def8; Int V2 = V2 by A2,TOPS_1:23; then reconsider V2 as a_neighborhood of x2 by A4,CONNSP_2:def 1; Int V1 = V1 by A1,TOPS_1:23; then reconsider V1 as a_neighborhood of x1 by A3,CONNSP_2:def 1; take V1,V2; Int V c= V by TOPS_1:16; hence thesis by A5; end; theorem Th32: for X being LinearTopSpace, a being Real, x being Point of X, V being a_neighborhood of a*x ex r being positive Real, W being a_neighborhood of x st for s being Real st |.s-a.| < r holds s*W c= V proof let X be LinearTopSpace, a be Real, x be Point of X, V be a_neighborhood of a*x; a*x in Int(V) by CONNSP_2:def 1; then consider r being positive Real, W being Subset of X such that A1: W is open and A2: x in W and A3: for s being Real st |.s-a.| < r holds s*W c= Int(V) by Def9; Int(W) = W by A1,TOPS_1:23; then reconsider W as a_neighborhood of x by A2,CONNSP_2:def 1; take r; take W; let s be Real; assume |.s-a.| < r; then A4: s*W c= Int(V) by A3; Int(V) c= V by TOPS_1:16; hence thesis by A4; end; definition let X be non empty RLTopStruct, a be Point of X; func transl(a,X) -> Function of X,X means :Def10: for x being Point of X holds it.x = a+x; existence proof deffunc F(Point of X) = a+\$1; consider F be Function of the carrier of X, the carrier of X such that A1: for x being Point of X holds F.x = F(x) from FUNCT_2:sch 4; reconsider F as Function of X,X; take F; thus thesis by A1; end; uniqueness proof let F,G be Function of X,X such that A2: for x being Point of X holds F.x = a+x and A3: for x being Point of X holds G.x = a+x; now let x be Point of X; thus F.x = a+x by A2 .= G.x by A3; end; hence F = G by FUNCT_2:63; end; end; theorem Th33: for X being non empty RLTopStruct, a being Point of X, V being Subset of X holds transl(a,X).:V = a+V proof let X be non empty RLTopStruct, a be Point of X, V be Subset of X; thus transl(a,X).:V c= a+V proof let y be object; assume y in transl(a,X).:V; then consider c being Point of X such that A1: c in V and A2: y = transl(a,X).c by FUNCT_2:65; y = a+c by A2,Def10; hence thesis by A1,Lm1; end; let x be object; assume x in a+V; then x in {a + u where u is Point of X: u in V} by RUSUB_4:def 8; then consider u being Point of X such that A3: x = a+u and A4: u in V; x = transl(a,X).u by A3,Def10; hence thesis by A4,FUNCT_2:35; end; theorem Th34: for X being LinearTopSpace, a being Point of X holds rng transl( a,X) = [#]X proof let X be LinearTopSpace, a be Point of X; thus rng transl(a,X) c= [#]X; let y be object; assume y in [#]X; then reconsider y as Point of X; transl(a,X).(-a+y) = a+(-a+y) by Def10 .= a+-a+y by RLVECT_1:def 3 .= 0.X+y by RLVECT_1:5 .= y; hence thesis by FUNCT_2:4; end; Lm8: for X being LinearTopSpace, a being Point of X holds transl(a,X) is one-to-one proof let X be LinearTopSpace, a be Point of X; now let x1,x2 be object such that A1: x1 in the carrier of X & x2 in the carrier of X and A2: transl(a,X).x1 = transl(a,X).x2; reconsider x19 = x1, x29 = x2 as Point of X by A1; transl(a,X).x1 = a+x19 & transl(a,X).x2 = a+x29 by Def10; hence x1 = x2 by A2,RLVECT_1:8; end; hence thesis by FUNCT_2:19; end; theorem Th35: for X being LinearTopSpace, a being Point of X holds transl(a,X) " = transl(-a,X) proof let X be LinearTopSpace, a be Point of X; A1: rng transl(a,X) = [#]X by Th34; now let x be Point of X; consider u being object such that A2: u in dom transl(a,X) and A3: x = transl(a,X).u by A1,FUNCT_1:def 3; reconsider u as Point of X by A2; A4: x = a+u by A3,Def10; transl(a,X) is onto one-to-one by A1,Lm8,FUNCT_2:def 3; hence transl(a,X)".x = (transl(a,X) qua Function)".x by TOPS_2:def 4 .= u by A3,Lm8,FUNCT_2:26 .= 0.X+u .= (-a+a)+u by RLVECT_1:5 .= -a+x by A4,RLVECT_1:def 3 .= transl(-a,X).x by Def10; end; hence thesis by FUNCT_2:63; end; Lm9: for X being LinearTopSpace, a being Point of X holds transl(a,X) is continuous proof let X be LinearTopSpace, a be Point of X; A1: now reconsider X9 = X as TopStruct; let P be Subset of X; defpred P[Subset of X9] means ex D being Subset of X st D = \$1 & D is open & a+D c= P; consider F being Subset-Family of X9 such that A2: for A being Subset of X9 holds A in F iff P[A] from SUBSET_1:sch 3; reconsider F as Subset-Family of X; assume A3: P is open; A4: union F = transl(a,X)"P proof thus union F c= transl(a,X)"P proof let x be object; assume x in union F; then consider A being set such that A5: x in A and A6: A in F by TARSKI:def 4; reconsider x as Point of X by A5,A6; A7: transl(a,X).x = a+x by Def10; consider D being Subset of X such that A8: D = A and D is open and A9: a+D c= P by A2,A6; a+D = {a + u where u is Point of X: u in D} by RUSUB_4:def 8; then a+x in a+D by A5,A8; hence thesis by A9,A7,FUNCT_2:38; end; let x be object; assume A10: x in transl(a,X)"P; then reconsider x as Point of X; transl(a,X).x in P by A10,FUNCT_2:38; then a+x in P by Def10; then consider V,D being Subset of X such that V is open and A11: D is open and A12: a in V and A13: x in D and A14: V+D c= P by A3,Def8; {a}+D = a+D & {a} c= V by A12,RUSUB_4:33,ZFMISC_1:31; then a+D c= V+D by Th10; then a+D c= P by A14; then D in F by A2,A11; hence thesis by A13,TARSKI:def 4; end; F is open proof let A be Subset of X; assume A in F; then ex D being Subset of X st D=A & D is open & a+D c= P by A2; hence thesis; end; hence transl(a,X)"P is open by A4,TOPS_2:19; end; [#]X <> {}; hence thesis by A1,TOPS_2:43; end; registration let X be LinearTopSpace, a be Point of X; cluster transl(a,X) -> being_homeomorphism; coherence proof thus dom transl(a,X) = [#]X by FUNCT_2:def 1; thus rng transl(a,X) = [#]X by Th34; thus transl(a,X) is one-to-one by Lm8; thus transl(a,X) is continuous by Lm9; transl(a,X)" = transl(-a,X) by Th35; hence thesis by Lm9; end; end; Lm10: for X being LinearTopSpace, E being Subset of X, x being Point of X st E is open holds x+E is open proof let X be LinearTopSpace, E be Subset of X, x be Point of X; assume A1: E is open; transl(x,X).:E = x+E by Th33; hence thesis by A1,TOPGRP_1:25; end; registration let X be LinearTopSpace, E be open Subset of X, x be Point of X; cluster x+E -> open; coherence by Lm10; end; Lm11: for X being LinearTopSpace, E being open Subset of X, K being Subset of X holds K+E is open proof let X be LinearTopSpace, E be open Subset of X, K be Subset of X; reconsider F = { a+E where a is Point of X: a in K} as Subset-Family of X by Lm2; A1: F is open proof let P be Subset of X; assume P in F; then ex a being Point of X st P=a+E & a in K; hence thesis; end; K+E = union F by Th4; hence thesis by A1,TOPS_2:19; end; registration let X be LinearTopSpace, E be open Subset of X, K be Subset of X; cluster K+E -> open; coherence by Lm11; end; Lm12: for X being LinearTopSpace, D being closed Subset of X, x being Point of X holds x+D is closed proof let X be LinearTopSpace, D be closed Subset of X, x be Point of X; transl(x,X).:D = x+D by Th33; hence thesis by TOPS_2:58; end; registration let X be LinearTopSpace, D be closed Subset of X, x be Point of X; cluster x+D -> closed; coherence by Lm12; end; theorem Th36: for X being LinearTopSpace, V1,V2,V being Subset of X st V1+V2 c= V holds Int V1 + Int V2 c= Int V proof let X be LinearTopSpace, V1,V2,V be Subset of X such that A1: V1+V2 c= V; Int V1 c= V1 & Int V2 c= V2 by TOPS_1:16; then Int V1 + Int V2 c= V1+V2 by Th11; then Int V1 + Int V2 c= V by A1; hence thesis by TOPS_1:24; end; theorem Th37: for X being LinearTopSpace, x being Point of X, V being Subset of X holds x+Int(V) = Int(x+V) proof let X be LinearTopSpace, x be Point of X, V be Subset of X; x+Int(V) c= x+V by Th8,TOPS_1:16; hence x+Int(V) c= Int(x+V) by TOPS_1:24; let v be object; assume A1: v in Int(x+V); then reconsider v as Point of X; consider Q being Subset of X such that A2: Q is open and A3: Q c= x+V and A4: v in Q by A1,TOPS_1:22; -x+Q c= -x+(x+V) by A3,Th8; then -x+Q c= -x+x+V by Th6; then -x+Q c= 0.X+V by RLVECT_1:5; then -x+Q c= V by Th5; then A5: x+Int(V) = {x + u where u is Point of X: u in Int V} & -x+Q c=Int(V) by A2, RUSUB_4:def 8,TOPS_1:24; -x+v in -x+Q by A4,Lm1; then x+(-x+v) in x+Int(V) by A5; then x+-x+v in x+Int(V) by RLVECT_1:def 3; then 0.X+v in x+Int(V) by RLVECT_1:5; hence thesis; end; theorem for X being LinearTopSpace, x being Point of X, V being Subset of X holds x+Cl(V) = Cl(x+V) proof let X be LinearTopSpace, x be Point of X, V be Subset of X; thus x+Cl(V) c= Cl(x+V) proof let v be object; assume A1: v in x+Cl(V); then reconsider v as Point of X; now A2: x+Cl(V) = {x + u where u is Point of X: u in Cl V} by RUSUB_4:def 8; A3: x+V = {x + u where u is Point of X: u in V} by RUSUB_4:def 8; let G be Subset of X such that A4: G is open and A5: v in G; A6: -x+G = {-x+u where u is Point of X: u in G} by RUSUB_4:def 8; then A7: -x+v in -x+G by A5; consider u being Point of X such that A8: v = x+u and A9: u in Cl V by A1,A2; -x+v = -x+x+u by A8,RLVECT_1:def 3 .= 0.X+u by RLVECT_1:5 .= u; then V meets -x+G by A4,A9,A7,PRE_TOPC:24; then consider z being object such that A10: z in V and A11: z in -x+G by XBOOLE_0:3; reconsider z as Point of X by A10; consider w being Point of X such that A12: z = -x+w and A13: w in G by A6,A11; A14: x+z in x+V by A3,A10; x+z = x+-x+w by A12,RLVECT_1:def 3 .= 0.X+w by RLVECT_1:5 .= w; hence x+V meets G by A13,A14,XBOOLE_0:3; end; hence thesis by PRE_TOPC:24; end; x+V c= x+Cl(V) by Th8,PRE_TOPC:18; hence thesis by TOPS_1:5; end; theorem for X being LinearTopSpace, x,v being Point of X, V being a_neighborhood of x holds v+V is a_neighborhood of v+x proof let X be LinearTopSpace, x,v be Point of X, V be a_neighborhood of x; v+Int(V) = {v + u where u is Point of X: u in Int V} & x in Int V by CONNSP_2:def 1,RUSUB_4:def 8; then A1: v+x in v+Int(V); v+Int(V) = Int(v+V) by Th37; hence thesis by A1,CONNSP_2:def 1; end; theorem for X being LinearTopSpace, x being Point of X, V being a_neighborhood of x holds -x+V is a_neighborhood of 0.X proof let X be LinearTopSpace, x be Point of X, V be a_neighborhood of x; -x+Int(V) = {-x + v where v is Point of X: v in Int V} & x in Int V by CONNSP_2:def 1,RUSUB_4:def 8; then -x+x in -x+Int(V); then A1: 0.X in -x+Int(V) by RLVECT_1:5; -x+Int(V) c= Int(-x+V) by Th37; hence thesis by A1,CONNSP_2:def 1; end; definition let X be non empty RLTopStruct; mode local_base of X is basis of 0.X; end; definition let X be non empty RLTopStruct; attr X is locally-convex means ex P being local_base of X st P is convex-membered; end; definition let X be LinearTopSpace, E be Subset of X; attr E is bounded means :Def12: for V being a_neighborhood of 0.X ex s st s > 0 & for t st t > s holds E c= t*V; end; registration let X be LinearTopSpace; cluster empty -> bounded for Subset of X; coherence proof let S be Subset of X; assume S is empty; then A1: S = {}X; let V be a_neighborhood of 0.X; take 1; thus thesis by A1; end; end; registration let X be LinearTopSpace; cluster bounded for Subset of X; existence proof take {}X; thus thesis; end; end; theorem Th41: for X being LinearTopSpace, V1,V2 being bounded Subset of X holds V1 \/ V2 is bounded proof let X be non empty LinearTopSpace, V1,V2 be bounded Subset of X; thus thesis proof let V be a_neighborhood of 0.X; consider s such that A1: s > 0 and A2: for t st t > s holds V1 c= t*V by Def12; consider r such that A3: r > 0 and A4: for t st t > r holds V2 c= t*V by Def12; per cases; suppose A5: r <= s; take s; thus s > 0 by A1; let t such that A6: t > s; t > r by A5,A6,XXREAL_0:2; then A7: V2 c= t*V by A4; V1 c= t*V by A2,A6; hence thesis by A7,XBOOLE_1:8; end; suppose A8: r > s; take r; thus r > 0 by A3; let t such that A9: t > r; t > s by A8,A9,XXREAL_0:2; then A10: V1 c= t*V by A2; V2 c= t*V by A4,A9; hence thesis by A10,XBOOLE_1:8; end; end; end; theorem for X being LinearTopSpace, P being bounded Subset of X, Q being Subset of X st Q c= P holds Q is bounded proof let X be LinearTopSpace, P be bounded Subset of X, Q being Subset of X such that A1: Q c= P; let V be a_neighborhood of 0.X; consider s such that A2: s > 0 and A3: for t st t > s holds P c= t*V by Def12; take s; thus s > 0 by A2; let t; assume t > s; then P c= t*V by A3; hence thesis by A1; end; theorem for X being LinearTopSpace, F being Subset-Family of X st F is finite & F = the set of all P where P is bounded Subset of X holds union F is bounded proof let X be LinearTopSpace, F be Subset-Family of X such that A1: F is finite and A2: F = the set of all P where P is bounded Subset of X; defpred P[set] means ex A being Subset of X st A = union \$1 & A is bounded; A3: now let P be Subset of X; assume P in F; then ex A being bounded Subset of X st P=A by A2; hence P is bounded; end; A4: for x,B being set st x in F & B c= F & P[B] holds P[B \/ {x}] proof let x,B be set such that A5: x in F and B c= F and A6: P[B]; consider A being Subset of X such that A7: A = union B & A is bounded by A6; reconsider x as Subset of X by A5; A8: union (B \/ {x}) = union B \/ union {x} by ZFMISC_1:78 .= union B \/ x by ZFMISC_1:25; A9: x is bounded by A3,A5; ex Y being Subset of X st Y = union (B \/ {x}) & Y is bounded proof take A \/ x; thus thesis by A7,A8,A9,Th41; end; hence thesis; end; {}X = union {} by ZFMISC_1:2; then A10: P[{}]; P[F] from FINSET_1:sch 2(A1,A10,A4); hence thesis; end; theorem Th44: for X being LinearTopSpace, P being Subset-Family of X st P = the set of all U where U is a_neighborhood of 0.X holds P is local_base of X proof let X be LinearTopSpace, P be Subset-Family of X such that A1: P = the set of all U where U is a_neighborhood of 0.X; let A be a_neighborhood of 0.X; take A; thus thesis by A1; end; theorem for X being LinearTopSpace, O being local_base of X, P being Subset-Family of X st P = {a+U where a is Point of X, U is Subset of X: U in O} holds P is basis of X proof let X be LinearTopSpace, O be basis of 0.X, P be Subset-Family of X such that A1: P = {a+U where a is Point of X, U is Subset of X: U in O}; let p be Point of X; let A be a_neighborhood of p; p in Int(A) by CONNSP_2:def 1; then -p+Int(A) is a_neighborhood of 0.X by Th9,CONNSP_2:3; then consider V being a_neighborhood of 0.X such that A2: V in O and A3: V c= -p+Int(A) by YELLOW13:def 2; take U = p+V; 0.X in Int(V) by CONNSP_2:def 1; then p+0.X in p+Int(V) by Lm1; then A4: p in p+Int(V); p+Int(V) c= Int(U) by Th37; hence U is a_neighborhood of p by A4,CONNSP_2:def 1; thus U in P by A1,A2; U c= p+(-p+Int(A)) by A3,Th8; then U c= p+-p+Int(A) by Th6; then U c= 0.X+Int(A) by RLVECT_1:5; then Int(A) c= A & U c= Int(A) by Th5,TOPS_1:16; hence thesis; end; definition let X be non empty RLTopStruct, r be Real; func mlt(r,X) -> Function of X,X means :Def13: for x being Point of X holds it.x = r*x; existence proof deffunc F(Point of X) = r*\$1; consider F be Function of the carrier of X, the carrier of X such that A1: for x being Point of X holds F.x = F(x) from FUNCT_2:sch 4; reconsider F as Function of X,X; take F; thus thesis by A1; end; uniqueness proof let F,G be Function of X,X such that A2: for x being Point of X holds F.x = r*x and A3: for x being Point of X holds G.x = r*x; now let x be Point of X; thus F.x = r*x by A2 .= G.x by A3; end; hence F = G by FUNCT_2:63; end; end; theorem Th46: for X being non empty RLTopStruct, V being Subset of X, r being non zero Real holds mlt(r,X).:V = r*V proof let X be non empty RLTopStruct, V be Subset of X, r be non zero Real; thus mlt(r,X).:V c= r*V proof let y be object; assume y in mlt(r,X).:V; then consider c being Point of X such that A1: c in V and A2: y = mlt(r,X).c by FUNCT_2:65; y = r*c by A2,Def13; hence thesis by A1; end; let x be object; assume x in r*V; then consider u being Point of X such that A3: x = r*u and A4: u in V; x = mlt(r,X).u by A3,Def13; hence thesis by A4,FUNCT_2:35; end; theorem Th47: for X being LinearTopSpace, r being non zero Real holds rng mlt( r,X) = [#]X proof let X be LinearTopSpace, r be non zero Real; thus rng mlt(r,X) c= [#]X; let y be object; assume y in [#]X; then reconsider y as Point of X; mlt(r,X).(r"*y) = r*(r"*y) by Def13 .= r*r"*y by RLVECT_1:def 7 .= 1*y by XCMPLX_0:def 7 .= y by RLVECT_1:def 8; hence thesis by FUNCT_2:4; end; Lm13: for X being LinearTopSpace, r being non zero Real holds mlt(r,X) is one-to-one proof let X be LinearTopSpace, r be non zero Real; now let x1,x2 be object such that A1: x1 in the carrier of X & x2 in the carrier of X and A2: mlt(r,X).x1 = mlt(r,X).x2; reconsider x19 = x1, x29 = x2 as Point of X by A1; mlt(r,X).x1 = r*x19 & mlt(r,X).x2 = r*x29 by Def13; hence x1 = x2 by A2,RLVECT_1:36; end; hence thesis by FUNCT_2:19; end; theorem Th48: for X being LinearTopSpace, r being non zero Real holds mlt(r,X) " = mlt(r",X) proof let X be LinearTopSpace, r be non zero Real; A1: rng mlt(r,X) = [#]X by Th47; now let x be Point of X; consider u being object such that A2: u in dom mlt(r,X) and A3: x = mlt(r,X).u by A1,FUNCT_1:def 3; reconsider u as Point of X by A2; A4: x = r*u by A3,Def13; mlt(r,X) is onto one-to-one by A1,Lm13,FUNCT_2:def 3; hence mlt(r,X)".x = (mlt(r,X) qua Function)".x by TOPS_2:def 4 .= u by A3,Lm13,FUNCT_2:26 .= 1*u by RLVECT_1:def 8 .= (r*r")*u by XCMPLX_0:def 7 .= r"*x by A4,RLVECT_1:def 7 .= mlt(r",X).x by Def13; end; hence thesis by FUNCT_2:63; end; Lm14: for X being LinearTopSpace, r being non zero Real holds mlt(r,X) is continuous proof let X be LinearTopSpace, r be non zero Real; A1: now let P be Subset of X; defpred P[Subset of X] means \$1 is open & r*\$1 c= P; consider F being Subset-Family of X such that A2: for A being Subset of X holds A in F iff P[A] from SUBSET_1:sch 3; reconsider F as Subset-Family of X; assume A3: P is open; A4: union F = mlt(r,X)"P proof thus union F c= mlt(r,X)"P proof let x be object; assume x in union F; then consider A being set such that A5: x in A and A6: A in F by TARSKI:def 4; reconsider A as Subset of X by A6; A is Subset of X; then reconsider x as Point of X by A5; A7: mlt(r,X).x = r*x by Def13; r*A c= P & r*x in r*A by A2,A5,A6; hence thesis by A7,FUNCT_2:38; end; let x be object; assume A8: x in mlt(r,X)"P; then reconsider x as Point of X; mlt(r,X).x in P by A8,FUNCT_2:38; then r*x in P by Def13; then consider e being positive Real, W being Subset of X such that A9: W is open and A10: x in W and A11: for s being Real st |.s - r.| < e holds s*W c= P by A3,Def9; |.r - r.| < e by ABSVALUE:2; then r*W c= P by A11; then W in F by A2,A9; hence thesis by A10,TARSKI:def 4; end; F is open by A2; hence mlt(r,X)"P is open by A4,TOPS_2:19; end; [#]X <> {}; hence thesis by A1,TOPS_2:43; end; registration let X be LinearTopSpace, r be non zero Real; cluster mlt(r,X) -> being_homeomorphism; coherence proof thus dom mlt(r,X) = [#]X by FUNCT_2:def 1; thus rng mlt(r,X) = [#]X by Th47; thus mlt(r,X) is one-to-one by Lm13; thus mlt(r,X) is continuous by Lm14; mlt(r,X)" = mlt(r",X) by Th48; hence thesis by Lm14; end; end; theorem Th49: for X being LinearTopSpace, V being open Subset of X, r being non zero Real holds r*V is open proof let X be LinearTopSpace, V be open Subset of X, r be non zero Real; reconsider r as non zero Real; mlt(r,X).:V = r*V by Th46; hence thesis by TOPGRP_1:25; end; theorem Th50: for X being LinearTopSpace, V being closed Subset of X, r being non zero Real holds r*V is closed proof let X be LinearTopSpace, V be closed Subset of X, r be non zero Real; reconsider r as non zero Real; mlt(r,X).:V = r*V by Th46; hence thesis by TOPS_2:58; end; theorem Th51: for X being LinearTopSpace, V being Subset of X, r be non zero Real holds r*Int(V) = Int(r*V) proof let X be LinearTopSpace, V be Subset of X, r be non zero Real; r*Int(V) c= r*V by CONVEX1:39,TOPS_1:16; hence r*Int(V) c= Int(r*V) by Th49,TOPS_1:24; let x be object; assume A1: x in Int(r*V); then reconsider x as Point of X; consider Q being Subset of X such that A2: Q is open and A3: Q c= r*V and A4: x in Q by A1,TOPS_1:22; r"*Q c= r"*(r*V) by A3,CONVEX1:39; then r"*Q c= r"*r*V by CONVEX1:37; then r"*Q c= 1*V by XCMPLX_0:def 7; then A5: r"*Q c= V by CONVEX1:32; r"*x in r"*Q & r"*Q is open by A2,A4,Th49; then r"*x in Int(V) by A5,TOPS_1:22; then r*(r"*x) in r*Int(V); then r*r"*x in r*Int(V) by RLVECT_1:def 7; then 1*x in r*Int(V) by XCMPLX_0:def 7; hence thesis by RLVECT_1:def 8; end; theorem Th52: for X being LinearTopSpace, A being Subset of X, r being non zero Real holds r*Cl(A) = Cl(r*A) proof let X be LinearTopSpace, A be Subset of X, r be non zero Real; thus r*Cl(A) c= Cl(r*A) proof let z be object; assume A1: z in r*Cl(A); then reconsider z as Point of X; now let G be Subset of X; assume G is open & z in G; then A2: r"*z in r"*G & r"*G is open by Th49; consider v being Point of X such that A3: z = r*v and A4: v in Cl A by A1; r"*z = r"*r*v by A3,RLVECT_1:def 7 .= 1*v by XCMPLX_0:def 7 .= v by RLVECT_1:def 8; then A meets r"*G by A4,A2,PRE_TOPC:24; then consider x being object such that A5: x in A and A6: x in r"*G by XBOOLE_0:3; reconsider x as Point of X by A5; consider u being Point of X such that A7: x = r"*u and A8: u in G by A6; A9: r*x in r*A by A5; r*x = r*r"*u by A7,RLVECT_1:def 7 .= 1*u by XCMPLX_0:def 7 .= u by RLVECT_1:def 8; hence r*A meets G by A8,A9,XBOOLE_0:3; end; hence thesis by PRE_TOPC:24; end; r*A c= r*Cl(A) by CONVEX1:39,PRE_TOPC:18; hence thesis by Th50,TOPS_1:5; end; theorem for X being LinearTopSpace,A being Subset of X st X is T_1 holds 0*Cl( A) = Cl(0*A) proof let X be LinearTopSpace, A be Subset of X such that A1: X is T_1; per cases; suppose A2: A is empty; then A3: Cl A = {}X by PRE_TOPC:22; hence 0*Cl(A) = {}X by CONVEX1:33 .= Cl(0*A) by A2,A3,CONVEX1:33; end; suppose A4: A is non empty; then Cl A is non empty by PRE_TOPC:18,XBOOLE_1:3; hence 0*Cl(A) = {0.X} by CONVEX1:34 .= Cl {0.X} by A1,YELLOW_8:26 .= Cl(0*A) by A4,CONVEX1:34; end; end; theorem Th54: for X being LinearTopSpace, x being Point of X, V being a_neighborhood of x, r be non zero Real holds r*V is a_neighborhood of r*x proof let X be LinearTopSpace, x be Point of X, V be a_neighborhood of x, r be non zero Real; x in Int(V) by CONNSP_2:def 1; then r*x in r*Int(V); hence r*x in Int(r*V) by Th51; end; theorem Th55: for X being LinearTopSpace, V being a_neighborhood of 0.X, r be non zero Real holds r*V is a_neighborhood of 0.X proof let X be LinearTopSpace, V be a_neighborhood of 0.X, r be non zero Real; r*V is a_neighborhood of r*0.X by Th54; hence thesis; end; Lm15: for X being LinearTopSpace, V being bounded Subset of X, r being Real holds r*V is bounded proof let X be LinearTopSpace, V be bounded Subset of X; let r be Real; per cases; suppose A1: r = 0; per cases; suppose V is empty; hence thesis by CONVEX1:33; end; suppose A2: V is non empty; let U be a_neighborhood of 0.X; take s = 1; thus s > 0; let t; assume t > s; then t*U is a_neighborhood of 0.X by Th55; then A3: 0.X in t*U by CONNSP_2:4; r*V = {0.X} by A1,A2,CONVEX1:34; hence thesis by A3,ZFMISC_1:31; end; end; suppose A4: r <> 0; let U be a_neighborhood of 0.X; (1/r)*U is a_neighborhood of 0.X by A4,Th55; then consider s such that A5: s > 0 and A6: for t st t > s holds V c= t*((1/r)*U) by Def12; take s; thus s > 0 by A5; let t; assume t > s; then r*V c= r*(t*((1/r)*U)) by A6,CONVEX1:39; then r*V c= r*(t*(1/r)*U) by CONVEX1:37; then r*V c= r*((1/r)*(t*U)) by CONVEX1:37; then r*V c= r*(1/r)*(t*U) by CONVEX1:37; then r*V c= 1*(t*U) by A4,XCMPLX_1:87; then A7: r*V c= t*U by CONVEX1:32; let x be object; assume x in r*V; hence thesis by A7; end; end; registration let X be LinearTopSpace, V be bounded Subset of X, r be Real; cluster r*V -> bounded; coherence by Lm15; end; theorem Th56: for X being LinearTopSpace, W being a_neighborhood of 0.X ex U being open a_neighborhood of 0.X st U is symmetric & U+U c= W proof let X be LinearTopSpace, W be a_neighborhood of 0.X; 0.X+0.X = 0.X; then consider V1 being a_neighborhood of 0.X, V2 being a_neighborhood of 0.X such that A1: V1+V2 c= W by Th31; set U = Int(V1) /\ Int(V2) /\ ((-1)*Int(V1)) /\ ((-1)*Int(V2)); A2: (-1)*Int(V1) is open & (-1)*Int(V2) is open by Th49; (-1)*V2 is a_neighborhood of 0.X by Th55; then 0.X in Int((-1)*V2) by CONNSP_2:def 1; then A3: 0.X in (-1)*Int(V2) by Th51; (-1)*V1 is a_neighborhood of 0.X by Th55; then 0.X in Int((-1)*V1) by CONNSP_2:def 1; then A4: 0.X in (-1)*Int(V1) by Th51; 0.X in Int V1 & 0.X in Int V2 by CONNSP_2:def 1; then 0.X in Int(V1) /\ Int(V2) by XBOOLE_0:def 4; then 0.X in Int(V1) /\ Int(V2) /\ ((-1)*Int(V1)) by A4,XBOOLE_0:def 4; then 0.X in U by A3,XBOOLE_0:def 4; then 0.X in Int(U) by A2,TOPS_1:23; then reconsider U as open a_neighborhood of 0.X by A2,CONNSP_2:def 1; take U; (-1)*(-1)*Int(V1) = Int(V1) by CONVEX1:32; then A5: (-1)*((-1)*Int(V1)) = Int(V1) by CONVEX1:37; (-1)*(-1)*Int(V2) = Int(V2) by CONVEX1:32; then A6: (-1)*((-1)*Int(V2)) = Int(V2) by CONVEX1:37; thus U = Int(V1) /\ Int(V2) /\ (((-1)*Int(V1)) /\ ((-1)*Int(V2))) by XBOOLE_1:16 .= (-1)*(Int(V1) /\ Int(V2)) /\ (Int(V1) /\ Int(V2)) by Th15 .= (-1)*(Int(V1) /\ Int(V2)) /\ ((-1)*((-1)*Int(V1) /\ ((-1)*Int(V2)))) by A5,A6,Th15 .= (-1)*(Int(V1) /\ Int(V2) /\ ((-1)*Int(V1) /\ ((-1)*Int(V2)))) by Th15 .= -U by XBOOLE_1:16; let x be object; assume x in U + U; then x in {u + v where u,v is Point of X: u in U & v in U} by RUSUB_4:def 9; then consider u,v being Point of X such that A7: u+v = x and A8: u in U and A9: v in U; A10: U = Int(V1) /\ Int(V2) /\ (((-1)*Int(V1)) /\ ((-1)*Int(V2))) by XBOOLE_1:16; then v in Int(V1) /\ Int(V2) by A9,XBOOLE_0:def 4; then A11: v in Int(V2) by XBOOLE_0:def 4; Int(V1) c= V1 & Int(V2) c= V2 by TOPS_1:16; then A12: Int(V1)+Int(V2) c= V1+V2 by Th11; u in Int(V1) /\ Int(V2) by A8,A10,XBOOLE_0:def 4; then u in Int(V1) by XBOOLE_0:def 4; then u+v in {u9+v9 where u9,v9 is Point of X: u9 in Int(V1) & v9 in Int(V2)} by A11; then u+v in Int(V1)+Int(V2) by RUSUB_4:def 9; then u+v in V1+V2 by A12; hence thesis by A1,A7; end; theorem Th57: for X being LinearTopSpace, K being compact Subset of X, C being closed Subset of X st K misses C ex V being a_neighborhood of 0.X st K+V misses C+V proof let X be LinearTopSpace, K be compact Subset of X, C be closed Subset of X such that A1: K misses C; per cases; suppose A2: K = {}; take V = [#]X; thus V is a_neighborhood of 0.X by TOPGRP_1:21; K+V = {} by A2,CONVEX1:40; hence thesis; end; suppose A3: K <> {}; set xV = { [x,Vx] where x is Point of X, Vx is open a_neighborhood of 0.X: x in K & Vx is symmetric & x+Vx+Vx+Vx misses C}; A4: now let x be Point of X such that A5: x in K; -x+C` = {-x + u where u is Point of X: u in C`} & K c= C` by A1, RUSUB_4:def 8,SUBSET_1:23; then -x+x in -x+C` by A5; then 0.X in -x+C` by RLVECT_1:5; then -x+C` is a_neighborhood of 0.X by CONNSP_2:3; then consider V9 being open a_neighborhood of 0.X such that V9 is symmetric and A6: V9+V9 c= -x+C` by Th56; consider Vx being open a_neighborhood of 0.X such that A7: Vx is symmetric and A8: Vx+Vx c= V9 by Th56; take Vx; thus Vx is symmetric by A7; Vx c= V9 proof let z be object; assume A9: z in Vx; then reconsider z as Point of X; 0.X in Vx by CONNSP_2:4; then z+0.X in Vx+Vx by A9,Th3; then z in Vx+Vx; hence thesis by A8; end; then Vx+(Vx+Vx) c= V9 + V9 by A8,Th11; then Vx+Vx+Vx c=-x+C` by A6; then x+(Vx+Vx+Vx) c= x+(-x+C`) by Th8; then x+Vx+(Vx+Vx) c= x+(-x+C`) by Th7; then x+Vx+Vx+Vx c= x+(-x+C`) by CONVEX1:36; then x+Vx+Vx+Vx c= x+-x+C` by Th6; then x+Vx+Vx+Vx c= 0.X+C` by RLVECT_1:def 10; then x+Vx+Vx+Vx c= C` by Th5; hence x+Vx+Vx+Vx misses C by SUBSET_1:23; end; A10: now consider x be object such that A11: x in K by A3,XBOOLE_0:def 1; reconsider x as Point of X by A11; consider Vx being open a_neighborhood of 0.X such that A12: Vx is symmetric & x+Vx+Vx+Vx misses C by A4,A11; take z = [x,Vx]; thus z in xV by A11,A12; end; defpred P[object,object] means ex v1,v2 being Point of X, V1,V2 being open a_neighborhood of 0.X st \$1 = [v1,V1] & \$2 = [v2,V2] & v1+V1 = v2+V2; A13: for x,y,z being object st P[x,y] & P[y,z] holds P[x,z] proof let x,y,z be object; given v1,v2 being Point of X, V1,V2 being open a_neighborhood of 0.X such that A14: x = [v1,V1] and A15: y = [v2,V2] and A16: v1+V1 = v2+V2; given w1,w2 being Point of X, W1,W2 being open a_neighborhood of 0.X such that A17: y = [w1,W1] and A18: z = [w2,W2] & w1+W1 = w2+W2; take v1,w2,V1,W2; v2 = w1 by A15,A17,XTUPLE_0:1; hence thesis by A14,A15,A16,A17,A18,XTUPLE_0:1; end; reconsider xV as non empty set by A10; A19: for x being object st x in xV holds P[x,x] proof let x be object; assume x in xV; then ex v being Point of X, V being open a_neighborhood of 0.X st x = [v ,V] & v in K & V is symmetric & v+V+V+V misses C; hence thesis; end; A20: for x,y being object st P[x,y] holds P[y,x]; consider eqR being Equivalence_Relation of xV such that A21: for x,y being object holds [x,y] in eqR iff x in xV & y in xV & P[x, y] from EQREL_1:sch 1(A19,A20,A13); now let X be set; assume X in Class eqR; then ex x being object st x in xV & X = Class(eqR,x) by EQREL_1:def 3; hence X <> {} by EQREL_1:20; end; then consider g being Function such that A22: dom g = Class eqR and A23: for X being set st X in Class eqR holds g.X in X by FUNCT_1:111; set xVV = rng g; set F = { x+Vx where x is Point of X, Vx is open a_neighborhood of 0.X: [x ,Vx] in xVV}; F c= bool the carrier of X proof let A be object; assume A in F; then ex x being Point of X, Vx being open a_neighborhood of 0.X st A = x +Vx & [x,Vx] in xVV; hence thesis; end; then reconsider F as Subset-Family of X; A24: F is Cover of K proof let x be object; assume A25: x in K; then reconsider x as Point of X; consider Vx being open a_neighborhood of 0.X such that A26: Vx is symmetric & x+Vx+Vx+Vx misses C by A4,A25; [x,Vx] in xV by A25,A26; then A27: Class(eqR,[x,Vx]) in Class eqR by EQREL_1:def 3; then A28: g.Class(eqR,[x,Vx]) in xVV by A22,FUNCT_1:def 3; x+0.X in x+Vx by Lm1,CONNSP_2:4; then A29: x in x+Vx; g.Class(eqR,[x,Vx]) in Class(eqR,[x,Vx]) by A23,A27; then [g.Class(eqR,[x,Vx]),[x,Vx]] in eqR by EQREL_1:19; then consider v1,v2 being Point of X, V1,V2 being open a_neighborhood of 0.X such that A30: g.Class(eqR,[x,Vx]) = [v1,V1] and A31: [x,Vx] = [v2,V2] and A32: v1+V1 = v2+V2 by A21; x = v2 & Vx = V2 by A31,XTUPLE_0:1; then x+Vx in F by A30,A32,A28; hence thesis by A29,TARSKI:def 4; end; F is open proof let P be Subset of X; assume P in F; then ex x being Point of X, Vx being open a_neighborhood of 0.X st P = x +Vx & [x,Vx] in xVV; hence thesis; end; then consider G being Subset-Family of X such that A33: G c= F and A34: G is Cover of K and A35: G is finite by A24,COMPTS_1:def 4; set FVx = {Vx where Vx is open a_neighborhood of 0.X: ex x being Point of X st x+Vx in G & [x,Vx] in xVV}; FVx c= bool the carrier of X proof let A be object; assume A in FVx; then ex Vx being open a_neighborhood of 0.X st A = Vx & ex x being Point of X st x+Vx in G & [x,Vx] in xVV; hence thesis; end; then reconsider FVx as Subset-Family of X; defpred P[object,object] means ex x being Point of X, Vx being open a_neighborhood of 0.X st \$1 = x+Vx & x+Vx in G & [x,Vx] in xVV & \$2 = Vx; A36: for x being object st x in G ex y being object st y in FVx & P[x,y] proof let x be object; assume A37: x in G; then x in F by A33; then consider z being Point of X, Vz being open a_neighborhood of 0.X such that A38: x = z+Vz & [z,Vz] in xVV; take Vz; thus thesis by A37,A38; end; consider f being Function of G,FVx such that A39: for x being object st x in G holds P[x,f.x] from FUNCT_2:sch 1(A36 ); set FxVxVx = {x+Vx+Vx where x is Point of X, Vx is open a_neighborhood of 0.X : x+Vx in G & [x,Vx] in xVV}; take V = meet FVx; A40: rng g c= xV proof let x be object; assume x in rng g; then consider y being object such that A41: y in dom g and A42: x = g.y by FUNCT_1:def 3; reconsider y as set by TARSKI:1; x in y by A22,A23,A41,A42; hence thesis by A22,A41; end; A43: for A being Subset of X st A in G ex x being Point of X, Vx being open a_neighborhood of 0.X st A = x+Vx & [x,Vx] in xVV proof let A be Subset of X; assume A in G; then A in F by A33; hence thesis; end; A44: now consider y be Point of X such that A45: y in K by A3,SUBSET_1:4; consider W being Subset of X such that y in W and A46: W in G by A34,A45,Th2; consider x being Point of X, Vx being open a_neighborhood of 0.X such that A47: W = x+Vx & [x,Vx] in xVV by A43,A46; Vx in FVx by A46,A47; hence ex z being set st z in FVx; end; then A48: dom f = G by FUNCT_2:def 1; A49: FVx c= rng f proof let z be object; assume z in FVx; then consider Vx being open a_neighborhood of 0.X such that A50: z = Vx and A51: ex x being Point of X st x+Vx in G & [x,Vx] in xVV; consider x being Point of X such that A52: x+Vx in G and A53: [x,Vx] in xVV by A51; consider v being Point of X, Vv being open a_neighborhood of 0.X such that A54: x+Vx = v+Vv and v+Vv in G and A55: [v,Vv] in xVV and A56: f.(x+Vx) = Vv by A39,A52; [[x,Vx],[v,Vv]] in eqR by A21,A40,A53,A54,A55; then [x,Vx] in Class(eqR,[v,Vv]) by EQREL_1:19; then A57: Class(eqR,[v,Vv]) = Class(eqR,[x,Vx]) by A40,A55,EQREL_1:23; consider A being object such that A58: A in dom g and A59: [x,Vx] = g.A by A53,FUNCT_1:def 3; consider a being object such that A60: a in xV and A61: A = Class(eqR,a) by A22,A58,EQREL_1:def 3; [x,Vx] in Class(eqR,a) by A22,A23,A58,A59,A61; then A62: Class(eqR,a) = Class(eqR,[x,Vx]) by A60,EQREL_1:23; consider B being object such that A63: B in dom g and A64: [v,Vv] = g.B by A55,FUNCT_1:def 3; consider b being object such that A65: b in xV and A66: B = Class(eqR,b) by A22,A63,EQREL_1:def 3; [v,Vv] in Class(eqR,b) by A22,A23,A63,A64,A66; then [x,Vx] = [v,Vv] by A57,A59,A64,A61,A65,A66,A62,EQREL_1:23; then Vx = Vv by XTUPLE_0:1; hence thesis by A48,A50,A52,A56,FUNCT_1:3; end; A67: for x being Point of X, Vx being open a_neighborhood of 0.X st x+Vx in G & [x,Vx] in xVV holds x in K & Vx is symmetric & x+Vx+Vx+Vx misses C proof let x be Point of X, Vx be open a_neighborhood of 0.X such that A68: x+Vx in G and A69: [x,Vx] in xVV; consider A being object such that A70: A in dom g and A71: [x,Vx] = g.A by A69,FUNCT_1:def 3; consider a being object such that A72: a in xV and A73: A = Class(eqR,a) by A22,A70,EQREL_1:def 3; [x,Vx] in Class(eqR,a) by A22,A23,A70,A71,A73; then A74: Class(eqR,a) = Class(eqR,[x,Vx]) by A72,EQREL_1:23; x+Vx in F by A33,A68; then consider v being Point of X, Vv being open a_neighborhood of 0.X such that A75: x+Vx = v+Vv and A76: [v,Vv] in xVV; [[x,Vx],[v,Vv]] in eqR by A21,A40,A69,A75,A76; then [x,Vx] in Class(eqR,[v,Vv]) by EQREL_1:19; then A77: Class(eqR,[v,Vv]) = Class(eqR,[x,Vx]) by A40,A76,EQREL_1:23; consider B being object such that A78: B in dom g and A79: [v,Vv] = g.B by A76,FUNCT_1:def 3; consider b being object such that A80: b in xV and A81: B = Class(eqR,b) by A22,A78,EQREL_1:def 3; [v,Vv] in Class(eqR,b) by A22,A23,A78,A79,A81; then A82: [x,Vx] = [v,Vv] by A77,A71,A79,A73,A80,A81,A74,EQREL_1:23; then A83: Vx = Vv by XTUPLE_0:1; [v,Vv] in xV by A40,A76; then consider u being Point of X, Vu being open a_neighborhood of 0.X such that A84: [u,Vu] = [v,Vv] and A85: u in K & Vu is symmetric & u+Vu+Vu+Vu misses C; Vv = Vu by A84,XTUPLE_0:1; hence thesis by A84,A85,A82,A83,XTUPLE_0:1; end; now let Z be set; hereby reconsider A = C+V as set; assume Z in {{}}; then A86: Z = {} by TARSKI:def 1; consider y be Point of X such that A87: y in K by A3,SUBSET_1:4; consider W being Subset of X such that y in W and A88: W in G by A34,A87,Th2; consider x being Point of X, Vx being open a_neighborhood of 0.X such that A89: W = x+Vx & [x,Vx] in xVV by A43,A88; A90: x+Vx+Vx+Vx misses C by A67,A88,A89; reconsider B = x+Vx+Vx as set; take A,B; thus A in {C+V} by TARSKI:def 1; thus B in FxVxVx by A88,A89; A91: Vx is symmetric by A67,A88,A89; now A92: C+V = {u + v where u,v is Point of X: u in C & v in V} by RUSUB_4:def 9; assume A meets B; then consider z being object such that A93: z in A and A94: z in B by XBOOLE_0:3; reconsider z as Point of X by A93; consider u,v being Point of X such that A95: z = u+v and A96: u in C and A97: v in V by A93,A92; Vx in FVx by A88,A89; then v in Vx by A97,SETFAM_1:def 1; then -v in Vx by A91,Th25; then A98: z+-v in x+Vx+Vx+Vx by A94,Th3; z+-v = u+(v+-v) by A95,RLVECT_1:def 3 .= u+0.X by RLVECT_1:5 .= u; hence contradiction by A90,A96,A98,XBOOLE_0:3; end; hence Z = A /\ B by A86; end; given A,B being set such that A99: A in {C+V} and A100: B in FxVxVx and A101: Z = A /\ B; A102: A = C+V by A99,TARSKI:def 1; consider x being Point of X, Vx being open a_neighborhood of 0.X such that A103: B = x+Vx+Vx and A104: x+Vx in G & [x,Vx] in xVV by A100; A105: x+Vx+Vx+Vx misses C by A67,A104; A106: Vx is symmetric by A67,A104; now A107: C+V = {u + v where u,v is Point of X: u in C & v in V} by RUSUB_4:def 9 ; assume A meets B; then consider z being object such that A108: z in A and A109: z in B by XBOOLE_0:3; reconsider z as Point of X by A99,A108; consider u,v being Point of X such that A110: z = u+v and A111: u in C and A112: v in V by A102,A108,A107; Vx in FVx by A104; then v in Vx by A112,SETFAM_1:def 1; then -v in Vx by A106,Th25; then A113: z+-v in x+Vx+Vx+Vx by A103,A109,Th3; z+-v = u+(v+-v) by A110,RLVECT_1:def 3 .= u+0.X by RLVECT_1:5 .= u; hence contradiction by A105,A111,A113,XBOOLE_0:3; end; then A /\ B = {}; hence Z in {{}} by A101,TARSKI:def 1; end; then INTERSECTION ({C+V}, FxVxVx) = {{}} by SETFAM_1:def 5; then union INTERSECTION ({C+V}, FxVxVx) = {} by ZFMISC_1:25; then (C+V) /\ union FxVxVx = {} by SETFAM_1:25; then A114: C+V misses union FxVxVx; A115: FVx is open proof let P be Subset of X; assume P in FVx; then ex Vx being open a_neighborhood of 0.X st P = Vx & ex x being Point of X st x+Vx in G& [x,Vx] in xVV; hence thesis; end; f"FVx is finite by A35,FINSET_1:1; then FVx is finite by A49,FINSET_1:9; then V is open by A115,TOPS_2:20; then A116: Int V = V by TOPS_1:23; now let A be set; assume A117: A in FVx; then reconsider A9=A as Subset of X; ex Vx being open a_neighborhood of 0.X st A = Vx & ex x being Point of X st x+Vx in G & [x,Vx] in xVV by A117; then Int A9 c= A9 & 0.X in Int A9 by CONNSP_2:def 1,TOPS_1:16; hence 0.X in A; end; then 0.X in V by A44,SETFAM_1:def 1; hence V is a_neighborhood of 0.X by A116,CONNSP_2:def 1; set FxVxV = {x+Vx+V where x is Point of X, Vx is open a_neighborhood of 0. X: x+Vx in G & [x,Vx] in xVV}; A118: union FxVxV c= union FxVxVx proof let z be object; assume z in union FxVxV; then consider Y being set such that A119: z in Y and A120: Y in FxVxV by TARSKI:def 4; consider x being Point of X, Vx being open a_neighborhood of 0.X such that A121: Y = x+Vx+V and A122: x+Vx in G & [x,Vx] in xVV by A120; A123: x+Vx+Vx in FxVxVx by A122; x+Vx+V = {u + v where u,v is Point of X: u in x+Vx & v in V} by RUSUB_4:def 9; then consider u,v being Point of X such that A124: z = u+v and A125: u in x+Vx and A126: v in V by A119,A121; Vx in FVx by A122; then v in Vx by A126,SETFAM_1:def 1; then u+v in x+Vx+Vx by A125,Th3; hence thesis by A124,A123,TARSKI:def 4; end; K+V c= union FxVxV proof let z be object; A127: K+V = {u + v where u,v is Point of X: u in K & v in V} by RUSUB_4:def 9; assume z in K+V; then consider u,v being Point of X such that A128: z = u+v and A129: u in K and A130: v in V by A127; consider Vu being Subset of X such that A131: u in Vu and A132: Vu in G by A34,A129,Th2; consider x being Point of X, Vx being open a_neighborhood of 0.X such that A133: Vu = x+Vx and A134: [x,Vx] in xVV by A43,A132; A135: x+Vx+V in FxVxV by A132,A133,A134; z in x+Vx+V by A128,A130,A131,A133,Th3; hence thesis by A135,TARSKI:def 4; end; hence thesis by A118,A114,XBOOLE_1:1,63; end; end; theorem Th58: for X being LinearTopSpace, B being local_base of X, V being a_neighborhood of 0.X ex W being a_neighborhood of 0.X st W in B & Cl W c= V proof let X be LinearTopSpace, B be local_base of X; let V be a_neighborhood of 0.X; set C = (Int V)`; set K = {0.X}; 0.X in Int V by CONNSP_2:def 1; then not 0.X in (Int V)` by XBOOLE_0:def 5; then consider P being a_neighborhood of 0.X such that A1: K+P misses C+P by Th57,ZFMISC_1:50; A2: 0.X in Int P by CONNSP_2:def 1; then reconsider P9 = Int P as open a_neighborhood of 0.X by CONNSP_2:3; K+P9 c= K+P & C+P9 c= C+P by Lm3,TOPS_1:16; then K+P9 misses C+P9 by A1,XBOOLE_1:64; then Cl(K+P9) misses C+P9 by TSEP_1:36; then Cl(K+P9) misses C by A2,Th12,XBOOLE_1:63; then Cl P9 misses C by CONVEX1:35; then A3: Cl P9 c= Int V by SUBSET_1:24; consider W being a_neighborhood of 0.X such that A4: W in B and A5: W c= P9 by YELLOW13:def 2; take W; thus W in B by A4; A6: Cl W c= Cl P9 by A5,PRE_TOPC:19; Int V c= V by TOPS_1:16; then Cl P9 c= V by A3; hence thesis by A6; end; theorem Th59: for X being LinearTopSpace, V being a_neighborhood of 0.X ex W being a_neighborhood of 0.X st Cl W c= V proof let X be LinearTopSpace, V be a_neighborhood of 0.X; set B = the set of all U where U is a_neighborhood of 0.X; B c= bool the carrier of X proof let A be object; assume A in B; then ex U being a_neighborhood of 0.X st A = U; hence thesis; end; then B is local_base of X by Th44; then consider W being a_neighborhood of 0.X such that W in B and A1: Cl W c= V by Th58; take W; thus thesis by A1; end; registration cluster T_1 -> Hausdorff for LinearTopSpace; coherence proof let X be LinearTopSpace; assume A1: X is T_1; let p, q be Point of X; assume A2: p <> q; {q} is closed by A1,URYSOHN1:19; then consider V being a_neighborhood of 0.X such that A3: {p}+V misses {q}+V by A2,Th57,ZFMISC_1:11; take p+Int(V),q+Int(V); A4: {p}+V = p+V & {q}+V = q+V by RUSUB_4:33; thus p+Int(V) is open & q+Int(V) is open; 0.X in Int(V) by CONNSP_2:def 1; then p+0.X in p+Int(V) & q+0.X in q+Int(V) by Lm1; hence p in p+Int(V) & q in q+Int(V); p+Int(V) c= p+V & q+Int(V) c= q+V by Th8,TOPS_1:16; hence thesis by A3,A4,XBOOLE_1:64; end; end; theorem for X being LinearTopSpace, A being Subset of X holds Cl A = meet the set of all A+V where V is a_neighborhood of 0.X proof let X be LinearTopSpace, A be Subset of X; set AV = the set of all A+V where V is a_neighborhood of 0.X; set V = the a_neighborhood of 0.X; A1: for x being Point of X, V being a_neighborhood of 0.X holds A meets x+ Int(V) iff x in A+(-1)*Int(V) proof let x be Point of X, V be a_neighborhood of 0.X; A2: A+(-1)*Int(V) = {a+v where a,v is Point of X: a in A & v in (-1)*Int( V)} by RUSUB_4:def 9; hereby assume A meets x+Int(V); then x in A+-Int(V) by Th24; hence x in A+(-1)*Int(V); end; assume x in A+(-1)*Int(V); then consider a,v being Point of X such that A3: x = a+v and A4: a in A and A5: v in (-1)*Int(V) by A2; consider v9 being Point of X such that A6: v = (-1)*v9 and A7: v9 in Int(V) by A5; -v = (-1)*v by RLVECT_1:16 .= (-1)*(-1)*v9 by A6,RLVECT_1:def 7 .= v9 by RLVECT_1:def 8; then A8: x+v9 = a + (v + (-v)) by A3,RLVECT_1:def 3 .= a+0.X by RLVECT_1:5 .= a; x+Int(V) = {x+w where w is Point of X: w in Int(V)} by RUSUB_4:def 8; then x+v9 in x+Int(V) by A7; hence thesis by A4,A8,XBOOLE_0:3; end; AV c= bool the carrier of X proof let x be object; assume x in AV; then ex V being a_neighborhood of 0.X st x = A+V; hence thesis; end; then reconsider AV9 = AV as Subset-Family of X; A9: for x being Point of X holds x in Cl A iff for V being a_neighborhood of 0.X holds A meets x+Int(V) proof let x be Point of X; hereby assume A10: x in Cl A; let V be a_neighborhood of 0.X; 0.X in Int(V) by CONNSP_2:def 1; then x+0.X in x+Int(V) by Lm1; then x in x+Int(V); hence A meets x+Int(V) by A10,TOPS_1:12; end; assume A11: for V being a_neighborhood of 0.X holds A meets x+Int(V); now let V be Subset of X such that A12: V is open and A13: x in V; A14: Int(-x+V) = -x+V by A12,TOPS_1:23; -x+x in -x+V by A13,Lm1; then 0.X in -x+V by RLVECT_1:5; then -x+V is a_neighborhood of 0.X by A14,CONNSP_2:def 1; then A meets x+(-x+V) by A11,A14; then A meets x+-x+V by Th6; then A meets 0.X+V by RLVECT_1:5; hence A meets V by Th5; end; hence thesis by TOPS_1:12; end; A15: A+V in AV; thus Cl A c= meet AV proof let x be object; assume A16: x in Cl A; then reconsider x as Point of X; now let Y be set; assume Y in AV; then consider V being a_neighborhood of 0.X such that A17: Y = A+V; A18: A+V = {a+v where a,v is Point of X: a in A & v in V} by RUSUB_4:def 9; A19: (-1)*V is a_neighborhood of 0.X by Th55; then A meets x+Int((-1)*V) by A9,A16; then A+(-1)*Int((-1)*V) = {a+v where a,v is Point of X: a in A & v in (- 1)*Int((-1 )*V)} & x in A+(-1)*Int(((-1)*V)) by A1,A19,RUSUB_4:def 9; then consider a,v being Point of X such that A20: x = a+v & a in A and A21: v in (-1)*Int((-1)*V); consider v9 being Point of X such that A22: v=(-1)*v9 and A23: v9 in Int((-1)*V) by A21; Int((-1)*V) c= (-1)*V by TOPS_1:16; then v9 in (-1)*V by A23; then consider v99 being Point of X such that A24: v9 = (-1)*v99 and A25: v99 in V; v = (-1)*(-1)*v99 by A22,A24,RLVECT_1:def 7 .= v99 by RLVECT_1:def 8; hence x in Y by A17,A18,A20,A25; end; hence thesis by A15,SETFAM_1:def 1; end; let x be object; assume A26: x in meet AV; meet AV9 c= the carrier of X; then reconsider x as Point of X by A26; now let V be a_neighborhood of 0.X; 0.X in Int(V) by CONNSP_2:def 1; then Int(V) is a_neighborhood of 0.X by CONNSP_2:3; then (-1)*Int(V) is a_neighborhood of 0.X by Th55; then A+(-1)*Int(V) in AV; then x in A+(-1)*Int(V) by A26,SETFAM_1:def 1; hence A meets x+Int(V) by A1; end; hence thesis by A9; end; theorem Th61: for X being LinearTopSpace, A,B being Subset of X holds Int A + Int B c= Int(A+B) proof let X be LinearTopSpace, A,B be Subset of X; Int A c= A & Int B c= B by TOPS_1:16; then Int A + Int B c= A+B by Th11; hence thesis by TOPS_1:24; end; theorem Th62: for X being LinearTopSpace, A,B being Subset of X holds Cl A + Cl B c= Cl(A+B) proof let X be LinearTopSpace, A,B be Subset of X; let z be object; assume A1: z in Cl A + Cl B; then reconsider z as Point of X; {u + v where u,v is Point of X: u in Cl A & v in Cl B} = Cl A + Cl B by RUSUB_4:def 9; then consider a,b being Point of X such that A2: z = a+b and A3: a in Cl A and A4: b in Cl B by A1; now let W be Subset of X such that A5: W is open and A6: z in W; W is a_neighborhood of z by A5,A6,CONNSP_2:3; then consider W1 being a_neighborhood of a, W2 being a_neighborhood of b such that A7: W1+W2 c= W by A2,Th31; a in Int W1 by CONNSP_2:def 1; then A meets Int W1 by A3,TOPS_1:12; then consider x being object such that A8: x in A and A9: x in Int W1 by XBOOLE_0:3; reconsider x as Point of X by A8; A10: Int W1 + Int W2 c= Int W by A7,Th36; b in Int W2 by CONNSP_2:def 1; then B meets Int W2 by A4,TOPS_1:12; then consider y being object such that A11: y in B and A12: y in Int W2 by XBOOLE_0:3; reconsider y as Point of X by A11; x+y in A+B & x+y in Int W1 + Int W2 by A8,A9,A11,A12,Th3; then A+B meets Int W by A10,XBOOLE_0:3; hence A+B meets W by A5,TOPS_1:23; end; hence thesis by TOPS_1:12; end; Lm16: for X being LinearTopSpace, C being convex Subset of X holds Cl C is convex proof let X be LinearTopSpace, C be convex Subset of X; now let r be Real such that A1: 0 < r and A2: r < 1; r*C + (1-r)*C c= C by A1,A2,CONVEX1:4; then A3: Cl(r*C + (1-r)*C) c= Cl(C) by PRE_TOPC:19; 0+r < 1 by A2; then 0 < 1-r by XREAL_1:20; then A4: (1-r)*Cl(C) = Cl((1-r)*C) by Th52; A5: Cl(r*C) + Cl((1-r)*C) c= Cl(r*C + (1-r)*C) by Th62; Cl(r*C) = r*Cl(C) by A1,Th52; hence r*Cl(C) + (1-r)*Cl(C) c= Cl(C) by A3,A5,A4; end; hence thesis by CONVEX1:4; end; registration let X be LinearTopSpace, C be convex Subset of X; cluster Cl C -> convex; coherence by Lm16; end; Lm17: for X being LinearTopSpace, C being convex Subset of X holds Int C is convex proof let X be LinearTopSpace, C be convex Subset of X; now let r be Real such that A1: 0 < r and A2: r < 1; r*C + (1-r)*C c= C by A1,A2,CONVEX1:4; then A3: Int(r*C + (1-r)*C) c= Int(C) by TOPS_1:19; 0+r < 1 by A2; then 0 < 1-r by XREAL_1:20; then A4: (1-r)*Int(C) = Int((1-r)*C) by Th51; A5: Int(r*C) + Int((1-r)*C) c= Int(r*C + (1-r)*C) by Th61; Int(r*C) = r*Int(C) by A1,Th51; hence r*Int(C) + (1-r)*Int(C) c= Int(C) by A3,A5,A4; end; hence thesis by CONVEX1:4; end; registration let X be LinearTopSpace, C be convex Subset of X; cluster Int C -> convex; coherence by Lm17; end; Lm18: for X being LinearTopSpace, B being circled Subset of X holds Cl B is circled proof let X be LinearTopSpace, B be circled Subset of X; let r be Real such that A1: |.r.| <= 1; per cases; suppose A2: r = 0; now per cases; suppose B = {}X; then Cl B = {}X by PRE_TOPC:22; hence thesis by CONVEX1:33; end; suppose A3: B <> {}X; A4: B c= Cl B by PRE_TOPC:18; A5: 0.X in B by A3,Th27; then r*Cl(B) = {0.X} by A2,A4,CONVEX1:34; hence thesis by A5,A4,ZFMISC_1:31; end; end; hence thesis; end; suppose A6: r <> 0; r*B c= B by A1,Def6; then Cl(r*B) c= Cl(B) by PRE_TOPC:19; hence thesis by A6,Th52; end; end; registration let X be LinearTopSpace, B be circled Subset of X; cluster Cl B -> circled; coherence by Lm18; end; theorem for X being LinearTopSpace, B being circled Subset of X st 0.X in Int B holds Int B is circled proof let X be LinearTopSpace, B be circled Subset of X such that A1: 0.X in Int B; let r be Real; assume |.r.| <= 1; then r*B c= B by Def6; then A2: Int(r*B) c= Int(B) by TOPS_1:19; per cases; suppose r = 0; then r*Int(B) = {0.X} by A1,CONVEX1:34; hence thesis by A1,ZFMISC_1:31; end; suppose r <> 0; hence thesis by A2,Th51; end; end; Lm19: for X being LinearTopSpace, E being bounded Subset of X holds Cl E is bounded proof let X be LinearTopSpace, E be bounded Subset of X; let V be a_neighborhood of 0.X; consider W be a_neighborhood of 0.X such that A1: Cl W c= V by Th59; consider s such that A2: s > 0 and A3: for t st t > s holds E c= t*W by Def12; take s; thus s > 0 by A2; let t; assume t > s; then A4: Cl E c= Cl(t*W) & Cl(t*W) = t*Cl(W) by A2,A3,Th52,PRE_TOPC:19; t*Cl(W) c= t*V by A1,CONVEX1:39; hence thesis by A4; end; registration let X be LinearTopSpace, E be bounded Subset of X; cluster Cl E -> bounded; coherence by Lm19; end; Lm20: for X being LinearTopSpace, U,V being a_neighborhood of 0.X, F being Subset-Family of X, r being positive Real st (for s being Real st |.s.| < r holds s*V c= U) & F = {a*V where a is Real: |.a.| < r} holds union F is a_neighborhood of 0.X & union F is circled & union F c= U proof let X be LinearTopSpace, U,V be a_neighborhood of 0.X, F be Subset-Family of X, r be positive Real such that A1: for s being Real st |.s.| < r holds s*V c= U and A2: F = {a*V where a is Real: |.a.| < r}; set W = union F; thus W is a_neighborhood of 0.X proof set F9 = {a*Int(V) where a is non zero Real: |.a.| < r}; consider a being Real such that A3: 0 < a and A4: a < r by XREAL_1:5; reconsider a as Real; 0.X in Int(V) by CONNSP_2:def 1; then a*0.X in a*Int(V); then A5: 0.X in a*Int(V); A6: F9 c= bool the carrier of X proof let A be object; assume A in F9; then ex a being non zero Real st A = a*Int(V) & |.a.| < r; hence thesis; end; |.a.| < r by A3,A4,ABSVALUE:def 1; then a*Int(V) in F9 by A3; then A7: 0.X in union F9 by A5,TARSKI:def 4; reconsider F9 as Subset-Family of X by A6; union F9 c= W proof let x be object; A8: Int V c= V by TOPS_1:16; assume x in union F9; then consider P being set such that A9: x in P and A10: P in F9 by TARSKI:def 4; consider a being non zero Real such that A11: P = a*Int(V) and A12: |.a.| < r by A10; ex v being Point of X st x = a*v & v in Int(V) by A9,A11; then A13: x in a*V by A8; a*V in F by A2,A12; hence thesis by A13,TARSKI:def 4; end; then A14: Int union F9 c= Int W by TOPS_1:19; F9 is open proof let P be Subset of X; assume P in F9; then ex a being non zero Real st P = a*Int(V) & |.a.| < r; hence thesis by Th49; end; then union F9 is open by TOPS_2:19; then 0.X in Int union F9 by A7,TOPS_1:23; hence 0.X in Int W by A14; end; thus W is circled proof let s be Real; assume |.s.| <= 1; then A15: |.s.|*r <= r by XREAL_1:153; let z be object; assume z in s*W; then consider u being Point of X such that A16: z = s*u and A17: u in W; consider Y being set such that A18: u in Y and A19: Y in F by A17,TARSKI:def 4; consider a being Real such that A20: Y = a*V and A21: |.a.| < r by A2,A19; consider v being Point of X such that A22: u = a*v and A23: v in V by A18,A20; z = s*a*v by A16,A22,RLVECT_1:def 7; then A24: z in s*a*V by A23; per cases; suppose 0 <> |.s.|; then s <> 0 by ABSVALUE:2; then 0 < |.s.| by COMPLEX1:47; then |.s.|*|.a.| < |.s.| * r by A21,XREAL_1:68; then |.s.|*|.a.| < r by A15,XXREAL_0:2; then |.s*a.| < r by COMPLEX1:65; then s*a*V in F by A2; hence thesis by A24,TARSKI:def 4; end; suppose |.s.| = 0; then s = 0 by ABSVALUE:2; then |.s*a.| = 0 by ABSVALUE:def 1; then s*a*V in F by A2; hence thesis by A24,TARSKI:def 4; end; end; let z be object; assume A25: z in W; then reconsider z as Point of X; consider Y being set such that A26: z in Y and A27: Y in F by A25,TARSKI:def 4; consider a being Real such that A28: Y = a*V and A29: |.a.| < r by A2,A27; a*V c= U by A1,A29; hence thesis by A26,A28; end; theorem Th64: for X being LinearTopSpace, U being a_neighborhood of 0.X ex W being a_neighborhood of 0.X st W is circled & W c= U proof let X be LinearTopSpace, U be a_neighborhood of 0.X; 0.X = 0*0.X; then consider r being positive Real, V being a_neighborhood of 0.X such that A1: for s being Real st |.s-0 .| < r holds s*V c= U by Th32; set F = {a*V where a is Real: |.a.| < r}; F c= bool the carrier of X proof let A be object; assume A in F; then ex a being Real st A = a*V & |.a.| < r; hence thesis; end; then reconsider F as Subset-Family of X; take union F; now let s be Real; assume |.s.| < r; then |.s-0 .| < r; hence s*V c= U by A1; end; hence thesis by Lm20; end; theorem for X being LinearTopSpace, U being a_neighborhood of 0.X st U is convex ex W being a_neighborhood of 0.X st W is circled convex & W c= U proof let X be LinearTopSpace, U be a_neighborhood of 0.X such that A1: U is convex; set V = U /\ -U; -U is a_neighborhood of 0.X by Th55; then reconsider V as a_neighborhood of 0.X by CONNSP_2:2; take V; A2: -U is convex by A1,CONVEX1:1; thus V is circled proof 0.X in V by CONNSP_2:4; then A3: 0.X in -U by XBOOLE_0:def 4; A4: 0.X in U by CONNSP_2:4; let r be Real such that A5: |.r.| <= 1; let u be object; assume u in r*V; then consider v being Point of X such that A6: u = r*v and A7: v in V; A8: v in -U by A7,XBOOLE_0:def 4; A9: v in U by A7,XBOOLE_0:def 4; per cases; suppose A10: r < 0; then A11: -r <= 1 by A5,ABSVALUE:def 1; then (-r)*v + (1--r)*0.X in -U by A2,A8,A3,A10; then (-r)*v + 0.X in -U; then (-r)*v in -U; then consider u9 being Point of X such that A12: (-r)*v = (-1)*u9 and A13: u9 in U; (-r)*v + (1--r)*0.X in U by A1,A9,A4,A10,A11; then (-r)*v + 0.X in U; then (-r)*v in U; then (-1)*(((-1)*r)*v) in (-1)*U; then A14: ((-1)*((-1)*r))*v in (-1)*U by RLVECT_1:def 7; u9 = ((-1)*(-1))*u9 by RLVECT_1:def 8 .= (-1)*((-1)*u9) by RLVECT_1:def 7 .= ((-r)*(-1))*v by A12,RLVECT_1:def 7 .= r*v; hence thesis by A6,A13,A14,XBOOLE_0:def 4; end; suppose A15: r >= 0; A16: r <= 1 by A5,ABSVALUE:def 1; then r*v + (1-r)*0.X in -U by A2,A8,A3,A15; then r*v + 0.X in -U; then A17: r*v in -U; r*v + (1-r)*0.X in U by A1,A9,A4,A15,A16; then r*v + 0.X in U; then r*v in U; hence thesis by A6,A17,XBOOLE_0:def 4; end; end; thus V is convex by A1,A2; thus thesis by XBOOLE_1:17; end; theorem for X being LinearTopSpace ex P being local_base of X st P is circled-membered proof let X be LinearTopSpace; defpred P[Subset of X] means \$1 is circled; consider P being Subset-Family of X such that A1: for V being Subset of X holds V in P iff P[V] from SUBSET_1:sch 3; reconsider P as Subset-Family of X; take P; thus P is local_base of X proof let V be a_neighborhood of 0.X; consider W being a_neighborhood of 0.X such that A2: W is circled and A3: W c= V by Th64; take W; thus W in P by A1,A2; thus thesis by A3; end; let V be Subset of X; assume V in P; hence thesis by A1; end; theorem for X being LinearTopSpace st X is locally-convex ex P being local_base of X st P is convex-membered; begin :: Addenda :: segments in a real vector space, 2009.04.01- A.T. reserve V for RealLinearSpace, v,w for Point of V; theorem Th68: :: TOPREAL1:6 v in LSeg(v,w) proof v = (1-0)*v by RLVECT_1:def 8 .= (1-0)*v + 0.V .= (1-0)*v + 0*w by RLVECT_1:10; hence thesis; end; theorem :: GOBOARD7:7 1/2*(v+w) in LSeg(v,w) proof 1/2*(v+w) = (1-1/2)*v+1/2*w by RLVECT_1:def 5; hence thesis; end; theorem :: TOPREAL1:7 LSeg(v,v) = {v} proof thus LSeg(v,v) c= {v} proof let a be object; assume a in LSeg(v,v); then consider r such that A1: a = (1-r)*v + r*v and 0 <= r and r <= 1; a = ((1-r)+r)*v by A1,RLVECT_1:def 6 .= v by RLVECT_1:def 8; hence thesis by TARSKI:def 1; end; v in LSeg(v,v) by Th68; hence thesis by ZFMISC_1:31; end; theorem :: JORDAN2C:47 0.V in LSeg(v,w) implies ex r st v = r*w or w = r*v proof assume 0.V in LSeg(v,w); then consider s being Real such that A1: 0.V= (1-s)*v + s*w and 0 <= s and s <= 1; -s*w=(1-s)*v by A1,RLVECT_1:6; then A2: (-s)*w =(1-s)*v by RLVECT_1:79; per cases; suppose A3: -s<>0; take r = (-s)"*(1-s); w = 1*w by RLVECT_1:def 8 .= (-s)"*(-s)*w by A3,XCMPLX_0:def 7 .= (-s)"*((-s)*w) by RLVECT_1:def 7 .= r*v by A2,RLVECT_1:def 7; hence thesis; end; suppose A4: -s=0; take -s; thus thesis by A2,A4,RLVECT_1:def 8; end; end; :: from EUCLID_4 (generalized), A.T. definition let V,v,w; func Line(v,w) -> Subset of V equals the set of all (1-r)*v + r*w ; coherence proof set A = the set of all (1-r)*v + r*w ; A c= the carrier of V proof let x be object; assume x in A; then ex r st x = (1-r)*v + r*w; hence x in the carrier of V; end; hence thesis; end; commutativity proof let S be Subset of V; let v,w; set A = the set of all (1-r)*w + r*v ; assume A1: S = the set of all (1-r)*v + r*w ; thus S c= A proof let e be object; assume e in S; then consider r such that A2: e = (1-r)*v + r*w by A1; e = (1-(1-r))*w + (1-r)*v by A2; hence e in A; end; let e be object; assume e in A; then consider r such that A3: e = (1-r)*w + r*v; e = (1-(1-r))*v + (1-r)*w by A3; hence e in S by A1; end; end; theorem Th72: v in Line(v,w) proof v = (1-0)*v + 0.V by RLVECT_1:def 8 .= (1-0)*v + 0*w by RLVECT_1:10; hence thesis; end; registration let V,v,w; cluster Line(v,w) -> non empty; coherence by Th72; end; theorem LSeg(v,w) c= Line(v,w) proof let e be object; assume e in LSeg(v,w); then ex r st e =(1-r)*v + r*w & 0 <= r & r <= 1; hence e in Line(v,w); end; reserve x1,x2,x3,x4,y1,y2 for Element of V; theorem Th74: y1 in Line(x1,x2) & y2 in Line(x1,x2) implies Line(y1,y2) c= Line(x1,x2) proof assume y1 in Line(x1,x2); then consider t such that A1: y1 = (1-t)*x1 + t*x2; assume y2 in Line(x1,x2); then consider s such that A2: y2 = (1-s)*x1 + s*x2; let z be object; assume z in Line(y1,y2); then consider u such that A3: z = (1-u)*y1 + u*y2; z = ((1-u)*((1-t)*x1)+(1-u)*(t*x2))+u*((1-s)*x1+s*x2) by A1,A2,A3,RLVECT_1:def 5 .= ((1-u)*((1-t)*x1)+(1-u)*(t*x2))+(u*((1-s)*x1)+u*(s*x2)) by RLVECT_1:def 5 .= (((1-u)*(1-t))*x1+(1-u)*(t*x2))+(u*((1-s)*x1)+u*(s*x2)) by RLVECT_1:def 7 .= (((1-u)*(1-t))*x1+((1-u)*t)*x2)+(u*((1-s)*x1)+u*(s*x2)) by RLVECT_1:def 7 .= (((1-u)*(1-t))*x1+((1-u)*t)*x2)+((u*(1-s))*x1+u*(s*x2)) by RLVECT_1:def 7 .= (((1-u)*(1-t))*x1+((1-u)*t)*x2)+((u*(1-s))*x1+(u*s)*x2) by RLVECT_1:def 7 .= ((1-u)*(1-t))*x1+(((1-u)*t)*x2+((u*(1-s))*x1+(u*s)*x2)) by RLVECT_1:def 3 .= ((1-u)*(1-t))*x1+((u*(1-s))*x1+(((1-u)*t)*x2+(u*s)*x2)) by RLVECT_1:def 3 .= (((1-u)*(1-t))*x1+(u*(1-s))*x1)+(((1-u)*t)*x2+(u*s)*x2) by RLVECT_1:def 3 .= ((1-u)*(1-t)+u*(1-s))*x1+(((1-u)*t)*x2+(u*s)*x2) by RLVECT_1:def 6 .= (1-(1*t-u*t+u*s))*x1+(1*t-u*t+u*s)*x2 by RLVECT_1:def 6; hence z in Line(x1,x2); end; theorem Th75: y1 in Line(x1,x2) & y2 in Line(x1,x2) & y1 <> y2 implies Line(y1,y2) = Line(x1,x2) proof assume A1: y1 in Line(x1,x2); then consider t such that A2: y1 = (1-t)*x1 + t*x2; assume A3: y2 in Line(x1,x2); then consider s such that A4: y2 = (1-s)*x1 + s*x2; assume y1<>y2; then A5: t-s<>0 by A2,A4; thus Line(y1,y2) c= Line(x1,x2) by A1,A3,Th74; (1-((t-1)/(t-s)))*y1 + ((t-1)/(t-s))*y2 = ((1*(t-s)-(t-1))/(t-s))*y1 + ( (t-1)/(t-s))*y2 by A5,XCMPLX_1:127 .= (((-s+1)/(t-s))*((1-t)*x1) + ((-s+1)/(t-s))*(t*x2)) + ((t-1)/(t-s))*( (1-s)*x1 + s*x2) by A2,A4,RLVECT_1:def 5 .= (((-s+1)/(t-s))*((1-t)*x1) + ((-s+1)/(t-s))*(t*x2)) + (((t-1)/(t-s))* ((1-s)*x1) + ((t-1)/(t-s))*(s*x2)) by RLVECT_1:def 5 .= ((((-s+1)/(t-s))*(1-t))*x1 + ((-s+1)/(t-s))*(t*x2)) + (((t-1)/(t-s))* ((1-s)*x1) + ((t-1)/(t-s))*(s*x2)) by RLVECT_1:def 7 .= ((((-s+1)/(t-s))*(1-t))*x1 + (((-s+1)/(t-s))*t)*x2) + (((t-1)/(t-s))* ((1-s)*x1) + ((t-1)/(t-s))*(s*x2)) by RLVECT_1:def 7 .= ((((-s+1)/(t-s))*(1-t))*x1 + (((-s+1)/(t-s))*t)*x2) + ((((t-1)/(t-s)) *(1-s))*x1 + ((t-1)/(t-s))*(s*x2)) by RLVECT_1:def 7 .= ((((-s+1)/(t-s))*(1-t))*x1 + (((-s+1)/(t-s))*t)*x2) + ((((t-1)/(t-s)) *(1-s))*x1 + (((t-1)/(t-s))*s)*x2) by RLVECT_1:def 7 .= (((-s+1)*(1-t))/(t-s))*x1 + ((((-s+1)*t)/(t-s))*x2 + ((((t-1)*(1-s))/ (t-s))*x1 + (((t-1)*s)/(t-s))*x2)) by RLVECT_1:def 3 .= (((-s+1)*(1-t))/(t-s))*x1 + ((((t-1)*(1-s))/(t-s))*x1 + ((((-s+1)*t)/ (t-s))*x2 + (((t-1)*s)/(t-s))*x2)) by RLVECT_1:def 3 .= ((((-s+1)*(1-t))/(t-s))*x1 + (((t-1)*(1-s))/(t-s))*x1) + ((((-s+1)*t) /(t-s))*x2 + (((t-1)*s)/(t-s))*x2) by RLVECT_1:def 3 .= (((-s+1)*(1-t))/(t-s) + ((t-1)*(1-s))/(t-s))*x1 + ((((-s+1)*t)/(t-s)) *x2 + (((t-1)*s)/(t-s))*x2) by RLVECT_1:def 6 .= (((-s+1)*(1-t))/(t-s) + ((t-1)*(1-s))/(t-s))*x1 + (((-s+1)*t)/(t-s) + ((t-1)*s)/(t-s))*x2 by RLVECT_1:def 6 .= 0.V + (((-s+1)*t + (t-1)*s)/(t-s))*x2 by RLVECT_1:10 .= (1*(t-s)/(t-s))*x2 .= 1*x2 by A5,XCMPLX_1:89 .= x2 by RLVECT_1:def 8; then A6: x2 in Line(y1,y2); (1-(t/(t-s)))*y1 + (t/(t-s))*y2 = ((1*(t-s)-t)/(t-s))*y1 + (t/(t-s))*y2 by A5,XCMPLX_1:127 .= (((-s)/(t-s))*((1-t)*x1) + ((-s)/(t-s))*(t*x2)) + (t/(t-s))*((1-s)*x1 + s*x2) by A2,A4,RLVECT_1:def 5 .= (((-s)/(t-s))*((1-t)*x1) + ((-s)/(t-s))*(t*x2)) + ((t/(t-s))*((1-s)* x1) + (t/(t-s))*(s*x2)) by RLVECT_1:def 5 .= ((((-s)/(t-s))*(1-t))*x1 + ((-s)/(t-s))*(t*x2)) + ((t/(t-s))*((1-s)* x1) + (t/(t-s))*(s*x2)) by RLVECT_1:def 7 .= ((((-s)/(t-s))*(1-t))*x1 + (((-s)/(t-s))*t)*x2) + ((t/(t-s))*((1-s)* x1) + (t/(t-s))*(s*x2)) by RLVECT_1:def 7 .= ((((-s)/(t-s))*(1-t))*x1 + (((-s)/(t-s))*t)*x2) + (((t/(t-s))*(1-s))* x1 + (t/(t-s))*(s*x2)) by RLVECT_1:def 7 .= ((((-s)/(t-s))*(1-t))*x1 + (((-s)/(t-s))*t)*x2) + (((t/(t-s))*(1-s))* x1 + ((t/(t-s))*s)*x2) by RLVECT_1:def 7 .= (((-s)*(1-t))/(t-s))*x1 + ((((-s)*t)/(t-s))*x2 + (((t*(1-s))/(t-s))* x1 + ((t*s)/(t-s))*x2)) by RLVECT_1:def 3 .= (((-s)*(1-t))/(t-s))*x1 + (((t*(1-s))/(t-s))*x1 + ((((-s)*t)/(t-s))* x2 + ((t*s)/(t-s))*x2)) by RLVECT_1:def 3 .= ((((-s)*(1-t))/(t-s))*x1 + ((t*(1-s))/(t-s))*x1) + ((((-s)*t)/(t-s))* x2 + ((t*s)/(t-s))*x2) by RLVECT_1:def 3 .= (((-s)*(1-t))/(t-s) + (t*(1-s))/(t-s))*x1 + ((((-s)*t)/(t-s))*x2 + (( t*s)/(t-s))*x2) by RLVECT_1:def 6 .= (((-s)*(1-t)+t*(1-s))/(t-s))*x1 + (((-s)*t)/(t-s) + (t*s)/(t-s))*x2 by RLVECT_1:def 6 .= (((-s)*(1-t)+t*(1-s))/(t-s))*x1 + 0.V by RLVECT_1:10 .= ((1*(t-s))/(t-s))*x1 .= 1*x1 by A5,XCMPLX_1:89 .= x1 by RLVECT_1:def 8; then x1 in Line(y1,y2); hence thesis by A6,Th74; end; :: 12.11.28, A.T. definition let V; let A be Subset of V; attr A is being_line means :Def15: ex x1,x2 st A=Line(x1,x2); end; registration let V; cluster being_line for Subset of V; existence proof set v = the Point of V; take Line(v,v),v,v; thus thesis; end; end; registration let V be non trivial RealLinearSpace; cluster non trivial being_line for Subset of V; existence proof consider v,w being Point of V such that A1: v <> w by STRUCT_0:def 10; take L=Line(v,w); thus L is non trivial proof take v,w; thus v in L & w in L by Th72; thus v <> w by A1; end; take v,w; thus thesis; end; end; definition let V; mode line of V is being_line Subset of V; end; definition let V; let x1,x2,x3 be Point of V; pred x1,x2,x3 are_collinear means ex L being line of V st x1 in L & x2 in L & x3 in L; end; definition let V; let x1,x2,x3,x4 be Point of V; pred x1,x2,x3,x4 are_collinear means ex L being line of V st x1 in L & x2 in L & x3 in L & x4 in L; end; theorem for x being object st x in LSeg(v,w) ex r st 0<=r & r<=1 & x=(1-r)*v+r*w proof let x be object; assume x in LSeg(v,w); then ex r st x = (1-r)*v + r*w & 0 <= r & r <= 1; hence ex r st 0<=r & r<=1 & x=(1-r)*v+r*w; end; theorem Th77: Line(v,v) = {v} proof for x being object holds x in Line(v,v) iff x = v proof let x be object; thus x in Line(v,v) implies x = v proof assume A1: x in Line(v,v); then reconsider w=x as Point of V; consider r such that A2: w = (1-r)*v + r*v by A1; w = ((1-r)+r)*v by A2,RLVECT_1:def 6; hence x = v by RLVECT_1:def 8; end; assume x = v; hence thesis by Th72; end; hence thesis by TARSKI:def 1; end; registration let V,v; cluster {v} -> being_line for Subset of V; coherence proof let A be Subset of V such that A1: A = {v}; take v,v; thus thesis by A1,Th77; end; let w; cluster Line(v,w) -> being_line; coherence; end; theorem for V being non trivial RealLinearSpace, L being non trivial line of V ex p,q being Point of V st p <> q & L = Line(p,q) proof let V be non trivial RealLinearSpace, L be non trivial line of V; consider p,q being object such that A1: p in L & q in L and A2: p <> q by ZFMISC_1:def 10; reconsider p,q as Point of V by A1; take p,q; thus p <> q by A2; ex x1,x2 being Element of V st L = Line(x1,x2) by Def15; hence L = Line(p,q) by A2,Th75,A1; end; theorem for x1,x2,x3,x4 be Point of V st x1,x2,x3,x4 are_collinear holds x1,x2,x3 are_collinear & x1,x2,x4 are_collinear; theorem Th80: for L being line of V, x1,x2 st x1 <> x2 & x1 in L & x2 in L holds L = Line(x1,x2) proof let L be line of V; ex x3,x4 st L = Line(x3,x4) by Def15; hence thesis by Th75; end; theorem for x1,x2,x3,x4 be Point of V st x1 <> x2 & x1,x2,x3 are_collinear & x1,x2,x4 are_collinear holds x1,x2,x3,x4 are_collinear proof let x1,x2,x3,x4 be Point of V such that A1: x1 <> x2; given L1 being line of V such that A2: x1 in L1 & x2 in L1 & x3 in L1; given L2 being line of V such that A3: x1 in L2 & x2 in L2 & x4 in L2; L1 = Line(x1,x2) & L2 = Line(x1,x2) by A1,A2,A3,Th80; hence ex L being line of V st x1 in L & x2 in L & x3 in L & x4 in L by A2,A3; end;