set V = {1};
reconsider empty1 = {} as Function of {},{1} by RELSET_1:12;
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 A1:
the
carrier of
G1 misses the
carrier of
G2
and A2:
G is_sum_of G1,
G2
;
contradiction
A3:
the
carrier of
G1 /\ the
carrier of
G2 = {}
by A1, XBOOLE_0:def 7;
A4:
( the
Source of
G1 tolerates the
Source of
G2 & the
Target of
G1 tolerates the
Target of
G2 )
by A2, Def4;
G = G1 \/ G2
by A2, Def4;
then A5:
the
carrier of
G1 \/ the
carrier of
G2 = {1}
by A4, Def3;
set x = the
Vertex of
G1;
( the
Vertex of
G1 in the
carrier of
G1 & the
Vertex of
G1 in {1} )
by A5, XBOOLE_0:def 3;
then A6:
1
in the
carrier of
G1
by TARSKI:def 1;
set y = the
Vertex of
G2;
( the
Vertex of
G2 in the
carrier of
G2 & the
Vertex of
G2 in {1} )
by A5, XBOOLE_0:def 3;
then
1
in the
carrier of
G2
by TARSKI:def 1;
hence
contradiction
by A3, A6, XBOOLE_0:def 4;
verum
end;
hence
G is connected
by Def8; verum