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 t1,s,V -separate t2,s

let V be Subset of (TOP-REAL n); :: thesis: for s, t1, t2 being Point of (TOP-REAL n) holds t1,s,V -separate t2,s

let s, t1, t2 be Point of (TOP-REAL n); :: thesis: t1,s,V -separate t2,s

let A be Subset of (TOP-REAL n); :: according to JORDAN18:def 3 :: thesis: ( A is_an_arc_of t1,s & A c= V implies A meets {t2,s} )

assume that

A1: A is_an_arc_of t1,s and

A c= V ; :: thesis: A meets {t2,s}

A2: s in {s,t2} by TARSKI:def 2;

s in A by A1, TOPREAL1:1;

hence A meets {t2,s} by A2, XBOOLE_0:3; :: thesis: verum

for s, t1, t2 being Point of (TOP-REAL n) holds t1,s,V -separate t2,s

let V be Subset of (TOP-REAL n); :: thesis: for s, t1, t2 being Point of (TOP-REAL n) holds t1,s,V -separate t2,s

let s, t1, t2 be Point of (TOP-REAL n); :: thesis: t1,s,V -separate t2,s

let A be Subset of (TOP-REAL n); :: according to JORDAN18:def 3 :: thesis: ( A is_an_arc_of t1,s & A c= V implies A meets {t2,s} )

assume that

A1: A is_an_arc_of t1,s and

A c= V ; :: thesis: A meets {t2,s}

A2: s in {s,t2} by TARSKI:def 2;

s in A by A1, TOPREAL1:1;

hence A meets {t2,s} by A2, XBOOLE_0:3; :: thesis: verum