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 f2 being Function of I[01] ,(T | Q) such that
A4: f2 is being_homeomorphism and
A5: f2 . 0 = p2 and
A6: f2 . 1 = q1 by A2, Def2;
consider f1 being Function of I[01] ,(T | P) such that
A7: f1 is being_homeomorphism and
A8: f1 . 0 = p1 and
A9: f1 . 1 = p2 by A1, Def2;
consider h being Function of I[01] ,(T | (P \/ Q)) such that
A10: h is being_homeomorphism and
A11: h . 0 = f1 . 0 and
A12: h . 1 = f2 . 1 by A3, A7, A9, 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 A8, A6, A10, A11, A12; :: thesis: verum