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:71;
hence LSeg q1,q2 is boundary by Th107; :: 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 set ; :: 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:13;
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

assume |.(q1 - q2).| = 0 ; :: thesis: contradiction
then q1 - q2 = 0. (TOP-REAL 2) by TOPRNS_1:25;
hence contradiction by A1, EUCLID:47; :: 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:60;
then consider r being real number such that
A9: r > 0 and
A10: Ball ez,r c= G1 by A8, TOPMETR:22;
reconsider r = r as Real by XREAL_0:def 1;
A11: r / 2 < r by A9, XREAL_1:218;
set p2 = (((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2 )),((q1 - q2) `1 )]|) + (((1 - s) * q1) + (s * q2));

now

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

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, EUCLID:52;
then A14: ((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2 )),((q1 - q2) `1 )]| = 0. (TOP-REAL 2) by EUCLID:46;
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, EUCLID:35, XCMPLX_1:6;
then A16: ( (0. (TOP-REAL 2)) `1 = - ((q1 - q2) `2 ) & (0. (TOP-REAL 2)) `2 = (q1 - q2) `1 ) by EUCLID:56;
( (0. (TOP-REAL 2)) `1 = 0 & (0. (TOP-REAL 2)) `2 = 0 ) by EUCLID:56, EUCLID:58;
hence contradiction by A1, A16, EUCLID:47, EUCLID:57, EUCLID:58; :: 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 EUCLID:52;
((((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, EUCLID:50
.= ((((1 - s2) * q1) - ((1 - s) * q1)) + (s2 * q2)) - (s * q2) by EUCLID:30
.= ((((1 - s2) - (1 - s)) * q1) + (s2 * q2)) - (s * q2) by EUCLID:54
.= ((s - s2) * q1) + ((s2 * q2) - (s * q2)) by EUCLID:49
.= ((s - s2) * q1) + ((s2 - s) * q2) by EUCLID:54
.= ((s - s2) * q1) + ((- (s - s2)) * q2)
.= ((s - s2) * q1) - ((s - s2) * q2) by EUCLID:44
.= (s - s2) * (q1 - q2) by EUCLID:53 ;
then ((1 / (s - s2)) * (s - s2)) * (q1 - q2) = (1 / (s - s2)) * (((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2 )),((q1 - q2) `1 )]|) by A17, EUCLID:34;
then 1 * (q1 - q2) = (1 / (s - s2)) * (((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2 )),((q1 - q2) `1 )]|) by A13, XCMPLX_1:107;
then q1 - q2 = (1 / (s - s2)) * (((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2 )),((q1 - q2) `1 )]|) by EUCLID:33;
then A18: q1 - q2 = ((1 / (s - s2)) * ((r / 2) / |.(q1 - q2).|)) * |[(- ((q1 - q2) `2 )),((q1 - q2) `1 )]| by EUCLID:34;
( (q1 - q2) `1 = |[(- ((q1 - q2) `2 )),((q1 - q2) `1 )]| `2 & - ((q1 - q2) `2 ) = |[(- ((q1 - q2) `2 )),((q1 - q2) `1 )]| `1 ) by EUCLID:56;
then q1 - q2 = 0. (TOP-REAL 2) by A18, Th108;
hence contradiction by A1, EUCLID:47; :: 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:13;
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 EUCLID:52;
A21: ( |[(- ((q1 - q2) `2 )),((q1 - q2) `1 )]| `1 = - ((q1 - q2) `2 ) & |[(- ((q1 - q2) `2 )),((q1 - q2) `1 )]| `2 = (q1 - q2) `1 ) by EUCLID:56;
|.((((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 EUCLID:50
.= |.(- (((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:27
.= (abs ((r / 2) / |.(q1 - q2).|)) * |.|[(- ((q1 - q2) `2 )),((q1 - q2) `1 )]|.| by TOPRNS_1:8
.= (abs ((r / 2) / |.(q1 - q2).|)) * (sqrt (((- ((q1 - q2) `2 )) ^2 ) + (((q1 - q2) `1 ) ^2 ))) by A21, JGRAPH_1:47
.= (abs ((r / 2) / |.(q1 - q2).|)) * (sqrt ((((q1 - q2) `1 ) ^2 ) + (((q1 - q2) `2 ) ^2 )))
.= (abs ((r / 2) / |.(q1 - q2).|)) * |.(q1 - q2).| by JGRAPH_1:47
.= ((abs (r / 2)) / (abs |.(q1 - q2).|)) * |.(q1 - q2).| by COMPLEX1:153
.= ((abs (r / 2)) / |.(q1 - q2).|) * |.(q1 - q2).| by ABSVALUE:def 1
.= abs (r / 2) by A5, XCMPLX_1:88
.= r / 2 by A9, ABSVALUE:def 1 ;
then dist ez,ep2 < r by A4, A11, JGRAPH_1:45;
then (((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2 )),((q1 - q2) `1 )]|) + (((1 - s) * q1) + (s * q2)) in Ball ez,r by METRIC_1:12;
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 13; :: 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:48;
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) by XBOOLE_0:def 10;
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;