theorem Th17: :: JORDAN20:17

for T being non empty TopStruct
for Q1, Q2 being Subset of T
for p1, p2 being Point of T st Q1 /\ Q2 = {} & Q1 \/ Q2 = the carrier of T & p1 in Q1 & p2 in Q2 & Q1 is open & Q2 is open holds
for P being Function of I[01],T holds
( not P is continuous or not P . 0 = p1 or not P . 1 = p2 )