set V = {1};
reconsider empty1 = {} as Function of {},{1} by RELSET_1:12;
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 ; :: thesis: ( G is non-multi & G is oriented & G is simple & G is connected )
thus G is non-multi ; :: thesis: ( G is oriented & G is simple & G is connected )
thus G is oriented ; :: thesis: ( G is simple & G is connected )
thus G is simple ; :: 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 and
A2: G is_sum_of G1,G2 ; :: thesis: 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;
G = G1 \/ G2 by A2;
then A5: the carrier of G1 \/ the carrier of G2 = {1} by A4, Def5;
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; :: thesis: verum
end;
hence G is connected ; :: thesis: verum