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