let q1, q2 be Point of (TOP-REAL 2); :: thesis: LSeg (q1,q2) is boundary

per cases ( q1 = q2 or q1 <> q2 ) ;

suppose q1 = q2 ; :: thesis: LSeg (q1,q2) is boundary

then LSeg (q1,q2) = {q1} by RLTOPSP1:70;
hence LSeg (q1,q2) is boundary by Th83; :: thesis: verum

end;

suppose A1: q1 <> q2 ; :: thesis: LSeg (q1,q2) is boundary

set P = LSeg (q1,q2);
the carrier of (TOP-REAL 2) c= Cl ((LSeg (q1,q2)) `)

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in the carrier of (TOP-REAL 2) or z in Cl ((LSeg (q1,q2)) `) )
assume A2: z in the carrier of (TOP-REAL 2) ; :: thesis: z in Cl ((LSeg (q1,q2)) `)

per cases ( z in LSeg (q1,q2) or not z in LSeg (q1,q2) ) ;

suppose A3: z in LSeg (q1,q2) ; :: thesis: z in Cl ((LSeg (q1,q2)) `)

reconsider ez = z as Point of (Euclid 2) by A2, TOPREAL3:8;
set p1 = q1 - q2;
consider s being Real such that
A4: z = ((1 - s) * q1) + (s * q2) and
0 <= s and
s <= 1 by A3;
set p = ((1 - s) * q1) + (s * q2);

A5: now :: thesis: not |.(q1 - q2).| = 0

assume |.(q1 - q2).| = 0 ; :: thesis: contradiction
then q1 - q2 = 0. (TOP-REAL 2) by TOPRNS_1:24;
hence contradiction by A1, RLVECT_1:21; :: thesis: verum

end;

for G1 being Subset of (TOP-REAL 2) st G1 is open & z in G1 holds
(LSeg (q1,q2)) ` meets G1

proof

let G1 be Subset of (TOP-REAL 2); :: thesis: ( G1 is open & z in G1 implies (LSeg (q1,q2)) ` meets G1 )
assume A6: G1 is open ; :: thesis: ( not z in G1 or (LSeg (q1,q2)) ` meets G1 )
thus ( z in G1 implies (LSeg (q1,q2)) ` meets G1 ) :: thesis: verum

proof

A7: TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2) by EUCLID:def 8;
then reconsider GG = G1 as Subset of (TopSpaceMetr (Euclid 2)) ;
assume A8: z in G1 ; :: thesis: (LSeg (q1,q2)) ` meets G1
GG is open by A6, A7, PRE_TOPC:30;
then consider r being Real such that
A9: r > 0 and
A10: Ball (ez,r) c= G1 by A8, TOPMETR:15;
reconsider r = r as Real ;
A11: r / 2 < r by A9, XREAL_1:216;
set p2 = (((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2)),((q1 - q2) `1)]|) + (((1 - s) * q1) + (s * q2));

now :: thesis: not (((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2)),((q1 - q2) `1)]|) + (((1 - s) * q1) + (s * q2)) in LSeg (q1,q2)

assume (((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2)),((q1 - q2) `1)]|) + (((1 - s) * q1) + (s * q2)) in LSeg (q1,q2) ; :: thesis: contradiction
then consider s2 being Real such that
A12: (((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2)),((q1 - q2) `1)]|) + (((1 - s) * q1) + (s * q2)) = ((1 - s2) * q1) + (s2 * q2) and
0 <= s2 and
s2 <= 1 ;

A13: now :: thesis: not s - s2 = 0

assume s - s2 = 0 ; :: thesis: contradiction
then ((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2)),((q1 - q2) `1)]| = (((1 - s) * q1) + (s * q2)) - (((1 - s) * q1) + (s * q2)) by A12, RLVECT_4:1;
then A14: ((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2)),((q1 - q2) `1)]| = 0. (TOP-REAL 2) by RLVECT_1:5;
A15: (r / 2) / |.(q1 - q2).| = (r * (2 ")) * (|.(q1 - q2).| ") by XCMPLX_0:def 9
.= r * ((2 ") * (|.(q1 - q2).| ")) ;
(2 ") * (|.(q1 - q2).| ") <> 0 by A5;
then |[(- ((q1 - q2) `2)),((q1 - q2) `1)]| = 0. (TOP-REAL 2) by A9, A14, A15, RLVECT_1:11, XCMPLX_1:6;
then A16: ( (0. (TOP-REAL 2)) `1 = - ((q1 - q2) `2) & (0. (TOP-REAL 2)) `2 = (q1 - q2) `1 ) ;
thus contradiction by A1, A16, EUCLID:53, EUCLID:54, RLVECT_1:21; :: thesis: verum

end;

A17: ((((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2)),((q1 - q2) `1)]|) + (((1 - s) * q1) + (s * q2))) - (((1 - s) * q1) + (s * q2)) = ((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2)),((q1 - q2) `1)]| by RLVECT_4:1;
((((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2)),((q1 - q2) `1)]|) + (((1 - s) * q1) + (s * q2))) - (((1 - s) * q1) + (s * q2)) = ((((1 - s2) * q1) + (s2 * q2)) - ((1 - s) * q1)) - (s * q2) by A12, RLVECT_1:27
.= ((((1 - s2) * q1) - ((1 - s) * q1)) + (s2 * q2)) - (s * q2) by RLVECT_1:def 3
.= ((((1 - s2) - (1 - s)) * q1) + (s2 * q2)) - (s * q2) by RLVECT_1:35
.= ((s - s2) * q1) + ((s2 * q2) - (s * q2)) by RLVECT_1:def 3
.= ((s - s2) * q1) + ((s2 - s) * q2) by RLVECT_1:35
.= ((s - s2) * q1) + ((- (s - s2)) * q2)
.= ((s - s2) * q1) - ((s - s2) * q2) by RLVECT_1:79
.= (s - s2) * (q1 - q2) by RLVECT_1:34 ;
then ((1 / (s - s2)) * (s - s2)) * (q1 - q2) = (1 / (s - s2)) * (((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2)),((q1 - q2) `1)]|) by A17, RLVECT_1:def 7;
then 1 * (q1 - q2) = (1 / (s - s2)) * (((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2)),((q1 - q2) `1)]|) by A13, XCMPLX_1:106;
then q1 - q2 = (1 / (s - s2)) * (((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2)),((q1 - q2) `1)]|) by RLVECT_1:def 8;
then A18: q1 - q2 = ((1 / (s - s2)) * ((r / 2) / |.(q1 - q2).|)) * |[(- ((q1 - q2) `2)),((q1 - q2) `1)]| by RLVECT_1:def 7;
( (q1 - q2) `1 = |[(- ((q1 - q2) `2)),((q1 - q2) `1)]| `2 & - ((q1 - q2) `2) = |[(- ((q1 - q2) `2)),((q1 - q2) `1)]| `1 ) ;
then q1 - q2 = 0. (TOP-REAL 2) by A18, Th84;
hence contradiction by A1, RLVECT_1:21; :: thesis: verum

end;

then A19: (((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2)),((q1 - q2) `1)]|) + (((1 - s) * q1) + (s * q2)) in the carrier of (TOP-REAL 2) \ (LSeg (q1,q2)) by XBOOLE_0:def 5;
reconsider ep2 = (((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2)),((q1 - q2) `1)]|) + (((1 - s) * q1) + (s * q2)) as Point of (Euclid 2) by TOPREAL3:8;
A20: ((((1 - s) * q1) + (s * q2)) + (- (((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2)),((q1 - q2) `1)]|))) - (((1 - s) * q1) + (s * q2)) = - (((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2)),((q1 - q2) `1)]|) by RLVECT_4:1;
A21: ( |[(- ((q1 - q2) `2)),((q1 - q2) `1)]| `1 = - ((q1 - q2) `2) & |[(- ((q1 - q2) `2)),((q1 - q2) `1)]| `2 = (q1 - q2) `1 ) ;
|.((((1 - s) * q1) + (s * q2)) - ((((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2)),((q1 - q2) `1)]|) + (((1 - s) * q1) + (s * q2)))).| = |.(((((1 - s) * q1) + (s * q2)) - (((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2)),((q1 - q2) `1)]|)) - (((1 - s) * q1) + (s * q2))).| by RLVECT_1:27
.= |.(- (((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2)),((q1 - q2) `1)]|)).| by A20
.= |.(((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2)),((q1 - q2) `1)]|).| by TOPRNS_1:26
.= |.((r / 2) / |.(q1 - q2).|).| * |.|[(- ((q1 - q2) `2)),((q1 - q2) `1)]|.| by TOPRNS_1:7
.= |.((r / 2) / |.(q1 - q2).|).| * (sqrt (((- ((q1 - q2) `2)) ^2) + (((q1 - q2) `1) ^2))) by A21, JGRAPH_1:30
.= |.((r / 2) / |.(q1 - q2).|).| * (sqrt ((((q1 - q2) `1) ^2) + (((q1 - q2) `2) ^2)))
.= |.((r / 2) / |.(q1 - q2).|).| * |.(q1 - q2).| by JGRAPH_1:30
.= (|.(r / 2).| / |.|.(q1 - q2).|.|) * |.(q1 - q2).| by COMPLEX1:67
.= (|.(r / 2).| / |.(q1 - q2).|) * |.(q1 - q2).| by ABSVALUE:def 1
.= |.(r / 2).| by A5, XCMPLX_1:87
.= r / 2 by A9, ABSVALUE:def 1 ;
then dist (ez,ep2) < r by A4, A11, JGRAPH_1:28;
then (((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2)),((q1 - q2) `1)]|) + (((1 - s) * q1) + (s * q2)) in Ball (ez,r) by METRIC_1:11;
hence (LSeg (q1,q2)) ` meets G1 by A10, A19, XBOOLE_0:3; :: thesis: verum

end;

end;

hence z in Cl ((LSeg (q1,q2)) `) by A2, PRE_TOPC:def 7; :: thesis: verum

end;

suppose A22: not z in LSeg (q1,q2) ; :: thesis: z in Cl ((LSeg (q1,q2)) `)

A23: (LSeg (q1,q2)) ` c= Cl ((LSeg (q1,q2)) `) by PRE_TOPC:18;
z in the carrier of (TOP-REAL 2) \ (LSeg (q1,q2)) by A2, A22, XBOOLE_0:def 5;
hence z in Cl ((LSeg (q1,q2)) `) by A23; :: thesis: verum

end;

end;

end;

then Cl ((LSeg (q1,q2)) `) = [#] (TOP-REAL 2) ;
then (LSeg (q1,q2)) ` is dense by TOPS_1:def 3;
hence LSeg (q1,q2) is boundary by TOPS_1:def 4; :: thesis: verum

end;

end;