let q, p 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 A1: ( q <> p & (LSeg q,p) /\ (L~ f) = {q} & p in L~ f ) ; :: thesis: contradiction
p in LSeg q,p by RLTOPSP1:69;
then p in {q} by A1, XBOOLE_0:def 4;
hence contradiction by A1, TARSKI:def 1; :: thesis: verum