consider EX being Point of (TOP-REAL 2) such that

A3: EX in P /\ Q and

A4: ex g being Function of I[01],((TOP-REAL 2) | P) ex s2 being Real st

( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = EX & 0 <= s2 & s2 <= 1 & ( for t being Real st 0 <= t & t < s2 holds

not g . t in Q ) ) by A1, A2, JORDAN5A:21;

EX in P by A3, XBOOLE_0:def 4;

then for g being Function of I[01],((TOP-REAL 2) | P)

for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = EX & 0 <= s2 & s2 <= 1 holds

for t being Real st 0 <= t & t < s2 holds

not g . t in Q by A4, Th1;

hence ex b_{1} being Point of (TOP-REAL 2) st

( b_{1} in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P)

for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b_{1} & 0 <= s2 & s2 <= 1 holds

for t being Real st 0 <= t & t < s2 holds

not g . t in Q ) ) by A3; :: thesis: verum

A3: EX in P /\ Q and

A4: ex g being Function of I[01],((TOP-REAL 2) | P) ex s2 being Real st

( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = EX & 0 <= s2 & s2 <= 1 & ( for t being Real st 0 <= t & t < s2 holds

not g . t in Q ) ) by A1, A2, JORDAN5A:21;

EX in P by A3, XBOOLE_0:def 4;

then for g being Function of I[01],((TOP-REAL 2) | P)

for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = EX & 0 <= s2 & s2 <= 1 holds

for t being Real st 0 <= t & t < s2 holds

not g . t in Q by A4, Th1;

hence ex b

( b

for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b

for t being Real st 0 <= t & t < s2 holds

not g . t in Q ) ) by A3; :: thesis: verum