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

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