let p, q be Point of (TOP-REAL 2); :: thesis: ( p <> q & ( p `1 = q `1 or p `2 = q `2 ) implies LSeg (p,q) is being_S-P_arc )
assume that
A1: p <> q and
A2: ( p `1 = q `1 or p `2 = q `2 ) ; :: thesis: LSeg (p,q) is being_S-P_arc
take f = <*p,q*>; :: according to TOPREAL1:def 9 :: thesis: ( f is being_S-Seq & LSeg (p,q) = L~ f )
thus f is being_S-Seq by A1, A2, Th43; :: thesis: LSeg (p,q) = L~ f
thus LSeg (p,q) = L~ f by Th21; :: thesis: verum