let T be T_2 TopSpace; :: thesis: for P, Q being Subset of T
for p1, p2, q1 being Point of T st P is_an_arc_of p1,p2 & Q is_an_arc_of p2,q1 & P /\ Q = {p2} holds
P \/ Q is_an_arc_of p1,q1
let P, Q be Subset of T; :: thesis: for p1, p2, q1 being Point of T st P is_an_arc_of p1,p2 & Q is_an_arc_of p2,q1 & P /\ Q = {p2} holds
P \/ Q is_an_arc_of p1,q1
let p1, p2, q1 be Point of T; :: thesis: ( P is_an_arc_of p1,p2 & Q is_an_arc_of p2,q1 & P /\ Q = {p2} implies P \/ Q is_an_arc_of p1,q1 )
assume that
A1: P is_an_arc_of p1,p2 and
A2: Q is_an_arc_of p2,q1 and
A3: P /\ Q = {p2} ; :: thesis: P \/ Q is_an_arc_of p1,q1
consider f1 being Function of I[01] ,(T | P) such that
A4: ( f1 is being_homeomorphism & f1 . 0 = p1 & f1 . 1 = p2 ) by A1, Def2;
consider f2 being Function of I[01] ,(T | Q) such that
A5: ( f2 is being_homeomorphism & f2 . 0 = p2 & f2 . 1 = q1 ) by A2, Def2;
consider h being Function of I[01] ,(T | (P \/ Q)) such that
A6: ( h is being_homeomorphism & h . 0 = f1 . 0 & h . 1 = f2 . 1 ) by A3, A4, A5, TOPMETR2:6;
take h ; :: according to TOPREAL1:def 2 :: thesis: ( h is being_homeomorphism & h . 0 = p1 & h . 1 = q1 )
thus ( h is being_homeomorphism & h . 0 = p1 & h . 1 = q1 ) by A4, A5, A6; :: thesis: verum