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