let p1, p2 be Point of (TOP-REAL 2); ( p1 <> p2 & p1 in R^2-unit_square & p2 in R^2-unit_square implies ex P1, P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} ) )
assume that
A1:
p1 <> p2
and
A2:
p1 in R^2-unit_square
and
A3:
p2 in R^2-unit_square
; ex P1, P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
A4:
( p1 in (LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|) or p1 in (LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|) )
by A2, TOPREAL1:def 4, XBOOLE_0:def 3;
per cases
( p1 in LSeg |[0 ,0 ]|,|[0 ,1]| or p1 in LSeg |[0 ,1]|,|[1,1]| or p1 in LSeg |[0 ,0 ]|,|[1,0 ]| or p1 in LSeg |[1,0 ]|,|[1,1]| )
by A4, XBOOLE_0:def 3;
end;