theorem Th4: :: BROUWER2:4

for n being Nat
for p, q being Point of (TOP-REAL n)
for A being convex Subset of (TOP-REAL n) st A is closed & p in Int A & p <> q & A /\ (halfline (p,q)) is bounded holds
ex u being Point of (TOP-REAL n) st (Fr A) /\ (halfline (p,q)) = {u}