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 v9 being Vertex of G ex e being Element of the carrier' of G st
( v9 in G -VSet X & not e in X & ( v9 = the Target of G . e or v9 = 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 v9 being Vertex of G ex e being Element of the carrier' of G st
( v9 in G -VSet X & not e in X & ( v9 = the Target of G . e or v9 = 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 v9 being Vertex of G ex e being Element of the carrier' of G st
( v9 in G -VSet X & not e in X & ( v9 = the Target of G . e or v9 = the Source of G . e ) ) )
assume that
A1: X meets the carrier' of G and
A2: not v in G -VSet X ; :: thesis: ex v9 being Vertex of G ex e being Element of the carrier' of G st
( v9 in G -VSet X & not e in X & ( v9 = the Target of G . e or v9 = the Source of G . e ) )
ex e being object st
( e in X & e in the carrier' of G ) by A1, XBOOLE_0:3;
then not G -VSet X is empty by Th17;
then consider vv being object such that
A3: vv in G -VSet X ;
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 and
A5: vs is_vertex_seq_of c and
A6: vs . 1 = vv and
A7: vs . (len vs) = v by A2, A3, Th18;
defpred S1[ Nat] means ( 1 <= $1 & $1 <= len c & not vs . ($1 + 1) in G -VSet X );
A8: len vs = (len c) + 1 by A5;
1 + 0 <= len c by A4, NAT_1:13;
then A9: ex n being Nat st S1[n] by A2, A7, A8;
consider k being Nat such that
A10: S1[k] and
A11: for n being Nat st S1[n] holds
k <= n from NAT_1:sch 5(A9);
 len c <= (len c) + 1 by NAT_1:11;
then k <= len vs by A8, A10, XXREAL_0:2;
then k in dom vs by A10, FINSEQ_3:25;
then reconsider v9 = vs . k as Vertex of G by FINSEQ_2:11;
reconsider c = c as FinSequence of the carrier' of G by MSSCYC_1:def 1;
A12: rng c c= the carrier' of G by FINSEQ_1:def 4;
k in dom c by A10, FINSEQ_3:25;
then c . k in rng c by FUNCT_1:def 3;
then reconsider e = c . k as Element of the carrier' of G by A12;
take v9 ; :: thesis: ex e being Element of the carrier' of G st
( v9 in G -VSet X & not e in X & ( v9 = the Target of G . e or v9 = the Source of G . e ) )
take e ; :: thesis: ( v9 in G -VSet X & not e in X & ( v9 = the Target of G . e or v9 = the Source of G . e ) )
hereby :: thesis: ( not e in X & ( v9 = the Target of G . e or v9 = the Source of G . e ) )
per cases ( k = 1 or 1 < k ) by A10, XXREAL_0:1;
suppose k = 1 ; :: thesis: v9 in G -VSet X
hence v9 in G -VSet X by A3, A6; :: thesis: verum
end;
suppose A13: 1 < k ; :: thesis: v9 in G -VSet X
assume A14: not v9 in G -VSet X ; :: thesis: contradiction
consider p being Element of NAT such that
A15: k = 1 + p and
A16: 1 <= p by A13, FINSEQ_4:84;
p <= k by A15, NAT_1:11;
then p <= len c by A10, XXREAL_0:2;
then k <= p by A11, A15, A16, A14;
hence contradiction by A15, NAT_1:13; :: thesis: verum
end;
end;
end;
hereby :: thesis: ( v9 = the Target of G . e or v9 = the Source of G . e )
( 1 <= k + 1 & k + 1 <= len vs ) by A8, A10, NAT_1:11, XREAL_1:6;
then k + 1 in dom vs by FINSEQ_3:25;
then reconsider v99 = vs . (k + 1) as Vertex of G by FINSEQ_2:11;
assume A17: e in X ; :: thesis: contradiction
( v99 = the Target of G . e or v99 = the Source of G . e ) by A5, A10, Lm3;
hence contradiction by A10, A17; :: thesis: verum
end;
thus ( v9 = the Target of G . e or v9 = the Source of G . e ) by A5, A10, Lm3; :: thesis: verum