let n be Element of NAT ; :: thesis: for V being Subset of
for t1, s, t2 being Point of holds t1,s,V -separate s,t2
let V be Subset of ; :: thesis: for t1, s, t2 being Point of holds t1,s,V -separate s,t2
let t1, s, t2 be Point of ; :: thesis: t1,s,V -separate s,t2
let A be Subset of ; :: according to JORDAN18:def 3 :: thesis: ( A is_an_arc_of t1,s & A c= V implies A meets {s,t2} )
assume that
A1: A is_an_arc_of t1,s and
A c= V ; :: thesis: A meets {s,t2}
A2: s in {s,t2} by TARSKI:def 2;
s in A by A1, TOPREAL1:4;
hence A meets {s,t2} by A2, XBOOLE_0:3; :: thesis: verum