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 2, 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;