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 )
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
;
hence
G is non-multi
by Def6; ( G is oriented & G is simple & G is connected )
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
;
hence
G is oriented
by Def5; ( G is simple & G is connected )
for x being set holds
( not x in the carrier' of G or not the Source of G . x = the Target of G . x )
;
hence
G is simple
by Def7; G is connected
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;
G = G1 \/ G2
by A6, Def4;
then A10:
the
carrier of
G1 \/ the
carrier of
G2 = {1}
by A8, Def3;
consider x being
Vertex of
G1;
(
x in the
carrier of
G1 &
x in {1} )
by A10, XBOOLE_0:def 3;
then A12:
1
in the
carrier of
G1
by TARSKI:def 1;
consider y being
Vertex of
G2;
(
y in the
carrier of
G2 &
y in {1} )
by A10, XBOOLE_0:def 3;
then
1
in the
carrier of
G2
by TARSKI:def 1;
hence
contradiction
by A7, A12, XBOOLE_0:def 4;
verum
end;
hence
G is connected
by Def8; verum