set V = {1};
reconsider empty1 = {} as Function of {} ,{1} by RELSET_1:25;
reconsider G = MultiGraphStruct(# {1},{} ,empty1,empty1 #) as Graph ;
take
G
; ( G is finite & G is non-multi & G is oriented & G is simple & G is connected )
thus
G is finite
by Def9; ( G is non-multi & G is oriented & G is simple & G is connected )
A1:
for x, y being set st x in the carrier' of G & y in the carrier' of G & ( ( the Source of G . x = the Source of G . y & the Target of G . x = the Target of G . y ) or ( the Source of G . x = the Target of G . y & the Source of G . y = the Target of G . x ) ) holds
x = y
;
thus
G is non-multi
by A1, Def6; ( G is oriented & G is simple & G is connected )
A2:
for x, y being set st x in the carrier' of G & y in the carrier' of G & the Source of G . x = the Source of G . y & the Target of G . x = the Target of G . y holds
x = y
;
thus
G is oriented
by A2, Def5; ( G is simple & G is connected )
A3:
for x being set holds
( not x in the carrier' of G or not the Source of G . x = the Target of G . x )
;
thus
G is simple
by A3, Def7; G is connected
A4:
for G1, G2 being Graph holds
( not the carrier of G1 misses the carrier of G2 or not G is_sum_of G1,G2 )
proof
given G1,
G2 being
Graph such that A5:
the
carrier of
G1 misses the
carrier of
G2
and A6:
G is_sum_of G1,
G2
;
contradiction
A7:
the
carrier of
G1 /\ the
carrier of
G2 = {}
by A5, XBOOLE_0:def 7;
A8:
( the
Source of
G1 tolerates the
Source of
G2 & the
Target of
G1 tolerates the
Target of
G2 )
by A6, Def4;
A9:
G = G1 \/ G2
by A6, Def4;
A10:
the
carrier of
G1 \/ the
carrier of
G2 = {1}
by A8, A9, Def3;
consider x being
Vertex of
G1;
A11:
(
x in the
carrier of
G1 &
x in {1} )
by A10, XBOOLE_0:def 3;
A12:
1
in the
carrier of
G1
by A11, TARSKI:def 1;
consider y being
Vertex of
G2;
A13:
(
y in the
carrier of
G2 &
y in {1} )
by A10, XBOOLE_0:def 3;
A14:
1
in the
carrier of
G2
by A13, TARSKI:def 1;
thus
contradiction
by A7, A12, A14, XBOOLE_0:def 4;
verum
end;
thus
G is connected
by A4, Def8; verum