let n be Element of NAT ; :: thesis: for V being Subset of
for t, s1, s2 being Point of holds t,t,V -separate s1,s2
let V be Subset of ; :: thesis: for t, s1, s2 being Point of holds t,t,V -separate s1,s2
let t, s1, s2 be Point of ; :: thesis: t,t,V -separate s1,s2
assume not t,t,V -separate s1,s2 ; :: thesis: contradiction
then ex A being Subset of st
( A is_an_arc_of t,t & A c= V & A misses {s1,s2} ) by Def3;
hence contradiction by JORDAN6:49; :: thesis: verum