let p, q be Point of (TOP-REAL 2); :: thesis: for f being FinSequence of (TOP-REAL 2) st q <> p & (LSeg (q,p)) /\ (L~ f) = {q} holds

not p in L~ f

let f be FinSequence of (TOP-REAL 2); :: thesis: ( q <> p & (LSeg (q,p)) /\ (L~ f) = {q} implies not p in L~ f )

assume that

A1: q <> p and

A2: ( (LSeg (q,p)) /\ (L~ f) = {q} & p in L~ f ) ; :: thesis: contradiction

p in LSeg (q,p) by RLTOPSP1:68;

then p in {q} by A2, XBOOLE_0:def 4;

hence contradiction by A1, TARSKI:def 1; :: thesis: verum

not p in L~ f

let f be FinSequence of (TOP-REAL 2); :: thesis: ( q <> p & (LSeg (q,p)) /\ (L~ f) = {q} implies not p in L~ f )

assume that

A1: q <> p and

A2: ( (LSeg (q,p)) /\ (L~ f) = {q} & p in L~ f ) ; :: thesis: contradiction

p in LSeg (q,p) by RLTOPSP1:68;

then p in {q} by A2, XBOOLE_0:def 4;

hence contradiction by A1, TARSKI:def 1; :: thesis: verum