consider EX being Point of (TOP-REAL 2) such that
A2: ( EX in P /\ Q & 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, JORDAN5A:22;
( EX in P & EX in Q ) by A2, 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 A2, Th1;
hence ex b₁ being Point of (TOP-REAL 2) st
( b₁ 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₁ & 0 <= s2 & s2 <= 1 holds
for t being Real st 0 <= t & t < s2 holds
not g . t in Q ) ) by A2; :: thesis: verum