let G be connected Graph; :: thesis: for X being set
for v being Vertex of G st X meets the carrier' of G & not v in G -VSet X holds
ex v' being Vertex of G ex e being Element of the carrier' of G st
( v' in G -VSet X & not e in X & ( v' = the Target of G . e or v' = the Source of G . e ) )
let X be set ; :: thesis: for v being Vertex of G st X meets the carrier' of G & not v in G -VSet X holds
ex v' being Vertex of G ex e being Element of the carrier' of G st
( v' in G -VSet X & not e in X & ( v' = the Target of G . e or v' = the Source of G . e ) )
let v be Vertex of G; :: thesis: ( X meets the carrier' of G & not v in G -VSet X implies ex v' being Vertex of G ex e being Element of the carrier' of G st
( v' in G -VSet X & not e in X & ( v' = the Target of G . e or v' = the Source of G . e ) ) )
assume A1: ( X meets the carrier' of G & not v in G -VSet X ) ; :: thesis: ex v' being Vertex of G ex e being Element of the carrier' of G st
( v' in G -VSet X & not e in X & ( v' = the Target of G . e or v' = the Source of G . e ) )
then consider e being set such that
A2: ( e in X & e in the carrier' of G ) by XBOOLE_0:3;
not G -VSet X is empty by A2, Th22;
then consider vv being set such that
A3: vv in G -VSet X by XBOOLE_0:def 1;
reconsider vv = vv as Vertex of G by A3;
consider c being Chain of G, vs being FinSequence of the carrier of G such that
A4: ( not c is empty & vs is_vertex_seq_of c & vs . 1 = vv & vs . (len vs) = v ) by A1, A3, Th23;
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= len c & not vs . ($1 + 1) in G -VSet X );
A5: len vs = (len c) + 1 by A4, GRAPH_2:def 7;
len c <> 0 by A4;
then 0 < len c ;
then 1 + 0 <= len c by NAT_1:13;
then A6: ex n being Nat st S₁[n] by A1, A4, A5;
consider k being Nat such that
A7: S₁[k] and
A8: for n being Nat st S₁[n] holds
k <= n from NAT_1:sch 5(A6);
len c <= (len c) + 1 by NAT_1:11;
then k <= len vs by A5, A7, XXREAL_0:2;
then k in dom vs by A7, FINSEQ_3:27;
then reconsider v' = vs . k as Vertex of G by FINSEQ_2:13;
take v' ; :: thesis: ex e being Element of the carrier' of G st
( v' in G -VSet X & not e in X & ( v' = the Target of G . e or v' = the Source of G . e ) )
reconsider c = c as FinSequence of the carrier' of G by MSSCYC_1:def 1;
k in dom c by A7, FINSEQ_3:27;
then A9: c . k in rng c by FUNCT_1:def 5;
rng c c= the carrier' of G by FINSEQ_1:def 4;
then reconsider e = c . k as Element of the carrier' of G by A9;
take e ; :: thesis: ( v' in G -VSet X & not e in X & ( v' = the Target of G . e or v' = the Source of G . e ) )

hereby :: thesis: ( not e in X & ( v' = the Target of G . e or v' = the Source of G . e ) )

per cases ( k = 1 or 1 < k ) by A7, XXREAL_0:1;

suppose k = 1 ; :: thesis: v' in G -VSet X

hence v' in G -VSet X by A3, A4; :: thesis: verum

end;

suppose 1 < k ; :: thesis: v' in G -VSet X

then consider p being Element of NAT such that
A10: ( k = 1 + p & 1 <= p ) by FSM_1:1;
assume A11: not v' in G -VSet X ; :: thesis: contradiction
p <= k by A10, NAT_1:11;
then p <= len c by A7, XXREAL_0:2;
then k <= p by A8, A10, A11;
hence contradiction by A10, NAT_1:13; :: thesis: verum

end;

end;

end;

hereby :: thesis: ( v' = the Target of G . e or v' = the Source of G . e )

assume A12: e in X ; :: thesis: contradiction
A13: 1 <= k + 1 by NAT_1:11;
k + 1 <= len vs by A5, A7, XREAL_1:8;
then k + 1 in dom vs by A13, FINSEQ_3:27;
then reconsider v'' = vs . (k + 1) as Vertex of G by FINSEQ_2:13;
( v'' = the Target of G . e or v'' = the Source of G . e ) by A4, A7, Lm3;
hence contradiction by A7, A12; :: thesis: verum

end;

thus ( v' = the Target of G . e or v' = the Source of G . e ) by A4, A7, Lm3; :: thesis: verum