theorem Th9: :: JORDAN5C:9

for P being Subset of (TOP-REAL 2)
for p1, p2, q1 being Point of (TOP-REAL 2) st q1 in P holds
LE q1,q1,P,p1,p2