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 z in LSeg q1,q2 ; :: thesis: z in Cl ((LSeg q1,q2) ` )

then z in { (((1 - s) * q1) + (s * q2)) where s is Real : ( 0 <= s & s <= 1 ) } ;
then consider s being Real such that
A3: ( z = ((1 - s) * q1) + (s * q2) & 0 <= s & s <= 1 ) ;
set p = ((1 - s) * q1) + (s * q2);
set p1 = q1 - q2;

A4: 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;

reconsider ez = z as Point of (Euclid 2) by A2, TOPREAL3:13;
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 A5: 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

assume Z: z in G1 ; :: thesis: (LSeg q1,q2) ` meets G1
X: 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)) ;
GG is open by A5, X, PRE_TOPC:60;
then consider r being real number such that
A6: ( r > 0 & Ball ez,r c= G1 ) by A5, Z, X, TOPMETR:22;
reconsider r = r as Real by XREAL_0:def 1;
A7: r / 2 > 0 by A6, XREAL_1:141;
set p2 = (((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2 )),((q1 - q2) `1 )]|) + (((1 - s) * q1) + (s * q2));
A8: ( |[(- ((q1 - q2) `2 )),((q1 - q2) `1 )]| `1 = - ((q1 - q2) `2 ) & |[(- ((q1 - q2) `2 )),((q1 - q2) `1 )]| `2 = (q1 - q2) `1 ) by EUCLID:56;
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;
U: ((((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;
A9: |.((((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 U, EUCLID:52
.= |.(((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 A8, 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 A4, XCMPLX_1:88
.= r / 2 by A7, ABSVALUE:def 1 ;
r / 2 < r by A6, XREAL_1:218;
then dist ez,ep2 < r by A3, A9, JGRAPH_1:45;
then A10: (((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2 )),((q1 - q2) `1 )]|) + (((1 - s) * q1) + (s * q2)) in Ball ez,r by METRIC_1:12;

now

assume (((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2 )),((q1 - q2) `1 )]|) + (((1 - s) * q1) + (s * q2)) in LSeg q1,q2 ; :: thesis: contradiction
then (((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2 )),((q1 - q2) `1 )]|) + (((1 - s) * q1) + (s * q2)) in { (((1 - s2) * q1) + (s2 * q2)) where s2 is Real : ( 0 <= s2 & s2 <= 1 ) } ;
then consider s2 being Real such that
A11: ( (((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2 )),((q1 - q2) `1 )]|) + (((1 - s) * q1) + (s * q2)) = ((1 - s2) * q1) + (s2 * q2) & 0 <= s2 & s2 <= 1 ) ;
A12: ((((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 A11, EUCLID:50
.= ((((1 - s2) * q1) - ((1 - s) * q1)) + (s2 * q2)) - (s * q2) by Th9
.= ((((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 ;
((((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;
then A13: ((1 / (s - s2)) * (s - s2)) * (q1 - q2) = (1 / (s - s2)) * (((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2 )),((q1 - q2) `1 )]|) by A12, EUCLID:34;

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 A11, EUCLID:52;
then A14: ((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2 )),((q1 - q2) `1 )]| = 0. (TOP-REAL 2) by EUCLID:46;
A15: (2 " ) * (|.(q1 - q2).| " ) <> 0 by A4;
(r / 2) / |.(q1 - q2).| = (r * (2 " )) * (|.(q1 - q2).| " ) by XCMPLX_0:def 9
.= r * ((2 " ) * (|.(q1 - q2).| " )) ;
then |[(- ((q1 - q2) `2 )),((q1 - q2) `1 )]| = 0. (TOP-REAL 2) by A6, 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;

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 A17: 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 A17, Th108;
hence contradiction by A1, EUCLID:47; :: thesis: verum

end;

then (((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;
hence (LSeg q1,q2) ` meets G1 by A6, A10, XBOOLE_0:3; :: thesis: verum

end;

end;

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

end;

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

then A18: z in the carrier of (TOP-REAL 2) \ (LSeg q1,q2) by A2, XBOOLE_0:def 5;
(LSeg q1,q2) ` c= Cl ((LSeg q1,q2) ` ) by PRE_TOPC:48;
hence z in Cl ((LSeg q1,q2) ` ) by A18; :: 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;