set pq = {p,q};
per cases ( p = q or p <> q ) ;
suppose A1: p = q ; :: thesis: halfline (p,q) is closed
{p} is closed by URYSOHN1:19;
hence halfline (p,q) is closed by ; :: thesis: verum
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 ;
then reconsider E = <*p,q*> as Enumeration of {p,q} by ;
set Apq = Affin {p,q};
set TRn = TOP-REAL n;
set TR1 = TOP-REAL 1;
set L = ;
A4: E . 1 = p by FINSEQ_1:44;
reconsider L = as Subset of R^1 by TOPMETR:17;
consider h being Function of (),R^1 such that
A5: for p being Point of () holds h . p = p /. 1 by JORDAN2B:1;
set B = { w where w is Element of (() | (Affin {p,q})) : (w |-- E) | 1 in h " L } ;
{ w where w is Element of (() | (Affin {p,q})) : (w |-- E) | 1 in h " L } c= [#] (() | (Affin {p,q}))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { w where w is Element of (() | (Affin {p,q})) : (w |-- E) | 1 in h " L } or x in [#] (() | (Affin {p,q})) )
assume x in { w where w is Element of (() | (Affin {p,q})) : (w |-- E) | 1 in h " L } ; :: thesis: x in [#] (() | (Affin {p,q}))
then ex w being Element of (() | (Affin {p,q})) st
( x = w & (w |-- E) | 1 in h " L ) ;
hence x in [#] (() | (Affin {p,q})) ; :: thesis: verum
end;
then reconsider B = { w where w is Element of (() | (Affin {p,q})) : (w |-- E) | 1 in h " L } as Subset of (() | (Affin {p,q})) ;
A6: [#] (() | (Affin {p,q})) = Affin {p,q} by PRE_TOPC:def 5;
A7: card {p,q} = 2 by ;
A8: h is being_homeomorphism by ;
then A9: dom h = [#] () by TOPGRP_1:24;
A10: halfline (p,q) c= B
proof
Carrier (q |-- {q}) c= {q} by RLVECT_2:def 6;
then not p in Carrier (q |-- {q}) by ;
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 ;
then 0 = (q |-- {p,q}) . p by ;
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 ;
A18: ( q in {p,q} & {p,q} c= Affin {p,q} ) by ;
then x |-- {p,q} = ((1 - a) * (p |-- {p,q})) + (a * (q |-- {p,q})) by ;
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
.= 1 - a by A17 ;
then (x |-- {p,q}) . p <= 1 - 0 by ;
then A19: (x |-- {p,q}) . p in L by XXREAL_1:234;
(1 - a) + a = 1 ;
then reconsider w = x as Element of (() | (Affin {p,q})) by ;
len (x |-- E) = 2 by ;
then A20: len ((x |-- E) | 1) = 1 by FINSEQ_1:59;
then reconsider wE1 = (x |-- E) | 1 as Point of () by TOPREAL3:46;
A21: 1 in dom wE1 by ;
then A22: ( wE1 /. 1 = wE1 . 1 & wE1 . 1 = (x |-- E) . 1 ) by ;
A23: 1 in dom (x |-- E) by ;
h . wE1 = wE1 /. 1 by A5;
then h . wE1 in L by ;
then wE1 in h " L by ;
then w in B ;
hence x in B ; :: thesis: verum
end;
L is closed by BORSUK_5:41;
then h " L is closed by ;
then A24: B is closed by ;
B c= halfline (p,q)
proof
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 (() | (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 () 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 ;
A30: 1 in dom (w |-- E) by ;
h . ((w |-- E) | 1) in L by ;
then (w |-- {p,q}) . p in L by ;
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 ;
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 ;
Sum (w |-- {p,q}) = w by ;
then w = ((1 - ((w |-- {p,q}) . q)) * p) + (((w |-- {p,q}) . q) * q) by ;
hence x in halfline (p,q) by ; :: thesis: verum
end;
then halfline (p,q) = B by A10;
hence halfline (p,q) is closed by ; :: thesis: verum
end;
end;