set V = {1};
reconsider empty1 = {} as Function of {} ,{1} by RELSET_1:25;
reconsider G = MultiGraphStruct(# {1},{} ,empty1,empty1 #) as Graph ;
take
G
; :: thesis: ( G is finite & G is non-multi & G is oriented & G is simple & G is connected )
thus
G is finite
by Def8; :: thesis: ( 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 Def5; :: thesis: ( 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 Def4; :: thesis: ( 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 Def6; :: thesis: 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 &
G is_sum_of G1,
G2 )
;
:: thesis: contradiction
A2:
the
carrier of
G1 /\ the
carrier of
G2 = {}
by A1, XBOOLE_0:def 7;
( the
Source of
G1 tolerates the
Source of
G2 & the
Target of
G1 tolerates the
Target of
G2 &
G = G1 \/ G2 )
by A1, Def3;
then A3:
the
carrier of
G1 \/ the
carrier of
G2 = {1}
by Def2;
consider x being
Vertex of
G1;
A5:
x in the
carrier of
G1
;
x in {1}
by A3, XBOOLE_0:def 3;
then A6:
1
in the
carrier of
G1
by A5, TARSKI:def 1;
consider y being
Vertex of
G2;
A8:
y in the
carrier of
G2
;
y in {1}
by A3, XBOOLE_0:def 3;
then
1
in the
carrier of
G2
by A8, TARSKI:def 1;
hence
contradiction
by A2, A6, XBOOLE_0:def 4;
:: thesis: verum
end;
hence
G is connected
by Def7; :: thesis: verum