set pq = {p,q};

per cases
( p = q or p <> q )
;

end;

suppose A2:
p <> q
; :: thesis: halfline (p,q) is closed

A3:
rng <*p,q*> = {p,q}
by FINSEQ_2:127;

<*p,q*> is one-to-one by A2, FINSEQ_3:94;

then reconsider E = <*p,q*> as Enumeration of {p,q} by A3, Def1;

set Apq = Affin {p,q};

set TRn = TOP-REAL n;

set TR1 = TOP-REAL 1;

set L = ].-infty,1.];

A4: E . 1 = p by FINSEQ_1:44;

reconsider L = ].-infty,1.] as Subset of R^1 by TOPMETR:17;

consider h being Function of (TOP-REAL 1),R^1 such that

A5: for p being Point of (TOP-REAL 1) holds h . p = p /. 1 by JORDAN2B:1;

set B = { w where w is Element of ((TOP-REAL n) | (Affin {p,q})) : (w |-- E) | 1 in h " L } ;

{ w where w is Element of ((TOP-REAL n) | (Affin {p,q})) : (w |-- E) | 1 in h " L } c= [#] ((TOP-REAL n) | (Affin {p,q}))

A6: [#] ((TOP-REAL n) | (Affin {p,q})) = Affin {p,q} by PRE_TOPC:def 5;

A7: card {p,q} = 2 by A2, CARD_2:57;

A8: h is being_homeomorphism by A5, JORDAN2B:28;

then A9: dom h = [#] (TOP-REAL 1) by TOPGRP_1:24;

A10: halfline (p,q) c= B

then h " L is closed by A8, TOPGRP_1:24;

then A24: B is closed by A7, Th28;

B c= halfline (p,q)

hence halfline (p,q) is closed by A6, A24, TSEP_1:8; :: thesis: verum

end;<*p,q*> is one-to-one by A2, FINSEQ_3:94;

then reconsider E = <*p,q*> as Enumeration of {p,q} by A3, Def1;

set Apq = Affin {p,q};

set TRn = TOP-REAL n;

set TR1 = TOP-REAL 1;

set L = ].-infty,1.];

A4: E . 1 = p by FINSEQ_1:44;

reconsider L = ].-infty,1.] as Subset of R^1 by TOPMETR:17;

consider h being Function of (TOP-REAL 1),R^1 such that

A5: for p being Point of (TOP-REAL 1) holds h . p = p /. 1 by JORDAN2B:1;

set B = { w where w is Element of ((TOP-REAL n) | (Affin {p,q})) : (w |-- E) | 1 in h " L } ;

{ w where w is Element of ((TOP-REAL n) | (Affin {p,q})) : (w |-- E) | 1 in h " L } c= [#] ((TOP-REAL n) | (Affin {p,q}))

proof

then reconsider B = { w where w is Element of ((TOP-REAL n) | (Affin {p,q})) : (w |-- E) | 1 in h " L } as Subset of ((TOP-REAL n) | (Affin {p,q})) ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { w where w is Element of ((TOP-REAL n) | (Affin {p,q})) : (w |-- E) | 1 in h " L } or x in [#] ((TOP-REAL n) | (Affin {p,q})) )

assume x in { w where w is Element of ((TOP-REAL n) | (Affin {p,q})) : (w |-- E) | 1 in h " L } ; :: thesis: x in [#] ((TOP-REAL n) | (Affin {p,q}))

then ex w being Element of ((TOP-REAL n) | (Affin {p,q})) st

( x = w & (w |-- E) | 1 in h " L ) ;

hence x in [#] ((TOP-REAL n) | (Affin {p,q})) ; :: thesis: verum

end;assume x in { w where w is Element of ((TOP-REAL n) | (Affin {p,q})) : (w |-- E) | 1 in h " L } ; :: thesis: x in [#] ((TOP-REAL n) | (Affin {p,q}))

then ex w being Element of ((TOP-REAL n) | (Affin {p,q})) st

( x = w & (w |-- E) | 1 in h " L ) ;

hence x in [#] ((TOP-REAL n) | (Affin {p,q})) ; :: thesis: verum

A6: [#] ((TOP-REAL n) | (Affin {p,q})) = Affin {p,q} by PRE_TOPC:def 5;

A7: card {p,q} = 2 by A2, CARD_2:57;

A8: h is being_homeomorphism by A5, JORDAN2B:28;

then A9: dom h = [#] (TOP-REAL 1) by TOPGRP_1:24;

A10: halfline (p,q) c= B

proof

L is closed
by BORSUK_5:41;
Carrier (q |-- {q}) c= {q}
by RLVECT_2:def 6;

then not p in Carrier (q |-- {q}) by A2, TARSKI:def 1;

then A11: (q |-- {q}) . p = 0 by RLVECT_2:19;

{q} is Affine by RUSUB_4:23;

then A12: Affin {q} = {q} by RLAFFIN1:50;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in halfline (p,q) or x in B )

set W = x |-- {p,q};

set wE = x |-- E;

A13: p in {p,q} by TARSKI:def 2;

assume x in halfline (p,q) ; :: thesis: x in B

then consider a being Real such that

A14: x = ((1 - a) * p) + (a * q) and

A15: 0 <= a by TOPREAL9:26;

reconsider a = a as Real ;

( q in {q} & {q} c= {p,q} ) by TARSKI:def 1, ZFMISC_1:36;

then 0 = (q |-- {p,q}) . p by A11, A12, RLAFFIN1:77;

then A16: (a * (q |-- {p,q})) . p = a * 0 by RLVECT_2:def 11

.= 0 ;

{p,q} c= conv {p,q} by CONVEX1:41;

then A17: (p |-- {p,q}) . p = 1 by A13, RLAFFIN1:72;

A18: ( q in {p,q} & {p,q} c= Affin {p,q} ) by RLAFFIN1:49, TARSKI:def 2;

then x |-- {p,q} = ((1 - a) * (p |-- {p,q})) + (a * (q |-- {p,q})) by A14, A13, RLAFFIN1:70;

then (x |-- {p,q}) . p = (((1 - a) * (p |-- {p,q})) . p) + ((a * (q |-- {p,q})) . p) by RLVECT_2:def 10

.= ((1 - a) * ((p |-- {p,q}) . p)) + 0 by A16, RLVECT_2:def 11

.= 1 - a by A17 ;

then (x |-- {p,q}) . p <= 1 - 0 by A15, XREAL_1:10;

then A19: (x |-- {p,q}) . p in L by XXREAL_1:234;

(1 - a) + a = 1 ;

then reconsider w = x as Element of ((TOP-REAL n) | (Affin {p,q})) by A6, A14, A13, A18, RLAFFIN1:78;

len (x |-- E) = 2 by A7, Th16;

then A20: len ((x |-- E) | 1) = 1 by FINSEQ_1:59;

then reconsider wE1 = (x |-- E) | 1 as Point of (TOP-REAL 1) by TOPREAL3:46;

A21: 1 in dom wE1 by A20, FINSEQ_3:25;

then A22: ( wE1 /. 1 = wE1 . 1 & wE1 . 1 = (x |-- E) . 1 ) by FUNCT_1:47, PARTFUN1:def 6;

A23: 1 in dom (x |-- E) by A21, RELAT_1:57;

h . wE1 = wE1 /. 1 by A5;

then h . wE1 in L by A4, A19, A22, A23, FUNCT_1:12;

then wE1 in h " L by A9, FUNCT_1:def 7;

then w in B ;

hence x in B ; :: thesis: verum

end;then not p in Carrier (q |-- {q}) by A2, TARSKI:def 1;

then A11: (q |-- {q}) . p = 0 by RLVECT_2:19;

{q} is Affine by RUSUB_4:23;

then A12: Affin {q} = {q} by RLAFFIN1:50;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in halfline (p,q) or x in B )

set W = x |-- {p,q};

set wE = x |-- E;

A13: p in {p,q} by TARSKI:def 2;

assume x in halfline (p,q) ; :: thesis: x in B

then consider a being Real such that

A14: x = ((1 - a) * p) + (a * q) and

A15: 0 <= a by TOPREAL9:26;

reconsider a = a as Real ;

( q in {q} & {q} c= {p,q} ) by TARSKI:def 1, ZFMISC_1:36;

then 0 = (q |-- {p,q}) . p by A11, A12, RLAFFIN1:77;

then A16: (a * (q |-- {p,q})) . p = a * 0 by RLVECT_2:def 11

.= 0 ;

{p,q} c= conv {p,q} by CONVEX1:41;

then A17: (p |-- {p,q}) . p = 1 by A13, RLAFFIN1:72;

A18: ( q in {p,q} & {p,q} c= Affin {p,q} ) by RLAFFIN1:49, TARSKI:def 2;

then x |-- {p,q} = ((1 - a) * (p |-- {p,q})) + (a * (q |-- {p,q})) by A14, A13, RLAFFIN1:70;

then (x |-- {p,q}) . p = (((1 - a) * (p |-- {p,q})) . p) + ((a * (q |-- {p,q})) . p) by RLVECT_2:def 10

.= ((1 - a) * ((p |-- {p,q}) . p)) + 0 by A16, RLVECT_2:def 11

.= 1 - a by A17 ;

then (x |-- {p,q}) . p <= 1 - 0 by A15, XREAL_1:10;

then A19: (x |-- {p,q}) . p in L by XXREAL_1:234;

(1 - a) + a = 1 ;

then reconsider w = x as Element of ((TOP-REAL n) | (Affin {p,q})) by A6, A14, A13, A18, RLAFFIN1:78;

len (x |-- E) = 2 by A7, Th16;

then A20: len ((x |-- E) | 1) = 1 by FINSEQ_1:59;

then reconsider wE1 = (x |-- E) | 1 as Point of (TOP-REAL 1) by TOPREAL3:46;

A21: 1 in dom wE1 by A20, FINSEQ_3:25;

then A22: ( wE1 /. 1 = wE1 . 1 & wE1 . 1 = (x |-- E) . 1 ) by FUNCT_1:47, PARTFUN1:def 6;

A23: 1 in dom (x |-- E) by A21, RELAT_1:57;

h . wE1 = wE1 /. 1 by A5;

then h . wE1 in L by A4, A19, A22, A23, FUNCT_1:12;

then wE1 in h " L by A9, FUNCT_1:def 7;

then w in B ;

hence x in B ; :: thesis: verum

then h " L is closed by A8, TOPGRP_1:24;

then A24: B is closed by A7, Th28;

B c= halfline (p,q)

proof

then
halfline (p,q) = B
by A10;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in halfline (p,q) )

assume x in B ; :: thesis: x in halfline (p,q)

then consider w being Element of ((TOP-REAL n) | (Affin {p,q})) such that

A25: x = w and

A26: (w |-- E) | 1 in h " L ;

set W = w |-- {p,q};

set wE = w |-- E;

reconsider wE1 = (w |-- E) | 1 as Point of (TOP-REAL 1) by A26;

A27: h . wE1 = wE1 /. 1 by A5;

len wE1 = 1 by CARD_1:def 7;

then A28: 1 in dom wE1 by FINSEQ_3:25;

then A29: ( wE1 /. 1 = wE1 . 1 & wE1 . 1 = (w |-- E) . 1 ) by FUNCT_1:47, PARTFUN1:def 6;

A30: 1 in dom (w |-- E) by A28, RELAT_1:57;

h . ((w |-- E) | 1) in L by A26, FUNCT_1:def 7;

then (w |-- {p,q}) . p in L by A4, A27, A29, A30, FUNCT_1:12;

then (w |-- {p,q}) . p <= 1 by XXREAL_1:234;

then A31: ((w |-- {p,q}) . p) - ((w |-- {p,q}) . p) <= 1 - ((w |-- {p,q}) . p) by XREAL_1:9;

A32: sum (w |-- {p,q}) = 1 by A6, RLAFFIN1:def 7;

Carrier (w |-- {p,q}) c= {p,q} by RLVECT_2:def 6;

then A33: sum (w |-- {p,q}) = ((w |-- {p,q}) . p) + ((w |-- {p,q}) . q) by A2, RLAFFIN1:33;

Sum (w |-- {p,q}) = w by A6, RLAFFIN1:def 7;

then w = ((1 - ((w |-- {p,q}) . q)) * p) + (((w |-- {p,q}) . q) * q) by A2, A33, A32, RLVECT_2:33;

hence x in halfline (p,q) by A25, A33, A32, A31, TOPREAL9:26; :: thesis: verum

end;assume x in B ; :: thesis: x in halfline (p,q)

then consider w being Element of ((TOP-REAL n) | (Affin {p,q})) such that

A25: x = w and

A26: (w |-- E) | 1 in h " L ;

set W = w |-- {p,q};

set wE = w |-- E;

reconsider wE1 = (w |-- E) | 1 as Point of (TOP-REAL 1) by A26;

A27: h . wE1 = wE1 /. 1 by A5;

len wE1 = 1 by CARD_1:def 7;

then A28: 1 in dom wE1 by FINSEQ_3:25;

then A29: ( wE1 /. 1 = wE1 . 1 & wE1 . 1 = (w |-- E) . 1 ) by FUNCT_1:47, PARTFUN1:def 6;

A30: 1 in dom (w |-- E) by A28, RELAT_1:57;

h . ((w |-- E) | 1) in L by A26, FUNCT_1:def 7;

then (w |-- {p,q}) . p in L by A4, A27, A29, A30, FUNCT_1:12;

then (w |-- {p,q}) . p <= 1 by XXREAL_1:234;

then A31: ((w |-- {p,q}) . p) - ((w |-- {p,q}) . p) <= 1 - ((w |-- {p,q}) . p) by XREAL_1:9;

A32: sum (w |-- {p,q}) = 1 by A6, RLAFFIN1:def 7;

Carrier (w |-- {p,q}) c= {p,q} by RLVECT_2:def 6;

then A33: sum (w |-- {p,q}) = ((w |-- {p,q}) . p) + ((w |-- {p,q}) . q) by A2, RLAFFIN1:33;

Sum (w |-- {p,q}) = w by A6, RLAFFIN1:def 7;

then w = ((1 - ((w |-- {p,q}) . q)) * p) + (((w |-- {p,q}) . q) * q) by A2, A33, A32, RLVECT_2:33;

hence x in halfline (p,q) by A25, A33, A32, A31, TOPREAL9:26; :: thesis: verum

hence halfline (p,q) is closed by A6, A24, TSEP_1:8; :: thesis: verum