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 11 :: thesis: ( f is being_S-Seq & LSeg p,q = L~ f )
thus f is being_S-Seq by A1, A2, Th46; :: thesis: LSeg p,q = L~ f
thus LSeg p,q = L~ f by Th21; :: thesis: verum