set V = {1,2};
set E = {1};
( 1 in {1,2} & 2 in {1,2} )
by TARSKI:def 2;
then reconsider S = {1} --> 1, T = {1} --> 2 as Function of {1},{1,2} by FUNCOP_1:45;
reconsider G = MultiGraphStruct(# {1,2},{1},S,T #) as Graph ;
take
G
; ( G is finite & G is simple & G is connected & not G is void & G is strict )
thus
G is finite
; ( G is simple & G is connected & not G is void & G is strict )
A1:
1 in {1}
by TARSKI:def 1;
then A2:
S . 1 = 1
by FUNCOP_1:7;
thus
G is simple
( G is connected & not G is void & G is strict )
A5:
T . 1 = 2
by A1, FUNCOP_1:7;
thus
G is connected
( not G is void & G is strict )proof
set MSG =
MultiGraphStruct(# the
carrier of
G, the
carrier' of
G, the
Source of
G, the
Target of
G #);
given G1,
G2 being
Graph such that A6:
the
carrier of
G1 misses the
carrier of
G2
and A7:
G is_sum_of G1,
G2
;
GRAPH_1:def 10 contradiction
A8:
MultiGraphStruct(# the
carrier of
G, the
carrier' of
G, the
Source of
G, the
Target of
G #)
= G1 \/ G2
by A7;
set V1 = the
carrier of
G1;
set V2 = the
carrier of
G2;
set T1 = the
Target of
G1;
set T2 = the
Target of
G2;
set S1 = the
Source of
G1;
set S2 = the
Source of
G2;
set E1 = the
carrier' of
G1;
set E2 = the
carrier' of
G2;
A9:
(rng the Source of G1) \/ (rng the Target of G1) c= the
carrier of
G1
by Th2;
A10:
(rng the Source of G2) \/ (rng the Target of G2) c= the
carrier of
G2
by Th2;
A11:
( the
Target of
G1 tolerates the
Target of
G2 & the
Source of
G1 tolerates the
Source of
G2 )
by A7;
then A12:
the
carrier of
MultiGraphStruct(# the
carrier of
G, the
carrier' of
G, the
Source of
G, the
Target of
G #)
= the
carrier of
G1 \/ the
carrier of
G2
by A8, GRAPH_1:def 5;
A13:
the
carrier' of
MultiGraphStruct(# the
carrier of
G, the
carrier' of
G, the
Source of
G, the
Target of
G #)
= the
carrier' of
G1 \/ the
carrier' of
G2
by A11, A8, GRAPH_1:def 5;
per cases
( ( the carrier' of G1 = {1} & the carrier' of G2 = {1} ) or ( the carrier' of G1 = {1} & the carrier' of G2 = {} ) or ( the carrier' of G1 = {} & the carrier' of G2 = {1} ) )
by A13, ZFMISC_1:37;
suppose A14:
( the
carrier' of
G1 = {1} & the
carrier' of
G2 = {1} )
;
contradictionthen
the
Source of
G2 . 1
= S . 1
by A1, A11, A8, GRAPH_1:def 5;
then
1
in rng the
Source of
G2
by A1, A2, A14, FUNCT_2:4;
then A15:
1
in (rng the Source of G2) \/ (rng the Target of G2)
by XBOOLE_0:def 3;
the
Source of
G1 . 1
= S . 1
by A1, A11, A8, A14, GRAPH_1:def 5;
then
1
in rng the
Source of
G1
by A1, A2, A14, FUNCT_2:4;
then
1
in (rng the Source of G1) \/ (rng the Target of G1)
by XBOOLE_0:def 3;
hence
contradiction
by A6, A9, A10, A15, XBOOLE_0:3;
verum end; suppose A16:
( the
carrier' of
G1 = {1} & the
carrier' of
G2 = {} )
;
contradictionthen
the
Target of
G1 . 1
= T . 1
by A1, A11, A8, GRAPH_1:def 5;
then
2
in rng the
Target of
G1
by A1, A5, A16, FUNCT_2:4;
then A17:
2
in (rng the Source of G1) \/ (rng the Target of G1)
by XBOOLE_0:def 3;
A18:
the
carrier of
G1 c= {1,2}
by A12, XBOOLE_1:7;
the
Source of
G1 . 1
= S . 1
by A1, A11, A8, A16, GRAPH_1:def 5;
then
1
in rng the
Source of
G1
by A1, A2, A16, FUNCT_2:4;
then
1
in (rng the Source of G1) \/ (rng the Target of G1)
by XBOOLE_0:def 3;
then
{1,2} c= the
carrier of
G1
by A9, A17, ZFMISC_1:32;
then
{1,2} = the
carrier of
G1
by A18, XBOOLE_0:def 10;
then
the
carrier of
G2 c= the
carrier of
G1
by A12, XBOOLE_1:7;
hence
contradiction
by A6, XBOOLE_1:67;
verum end; suppose A19:
( the
carrier' of
G1 = {} & the
carrier' of
G2 = {1} )
;
contradictionthen
the
Target of
G2 . 1
= T . 1
by A1, A11, A8, GRAPH_1:def 5;
then
2
in rng the
Target of
G2
by A1, A5, A19, FUNCT_2:4;
then A20:
2
in (rng the Source of G2) \/ (rng the Target of G2)
by XBOOLE_0:def 3;
A21:
the
carrier of
G2 c= {1,2}
by A12, XBOOLE_1:7;
the
Source of
G2 . 1
= S . 1
by A1, A11, A8, A19, GRAPH_1:def 5;
then
1
in rng the
Source of
G2
by A1, A2, A19, FUNCT_2:4;
then
1
in (rng the Source of G2) \/ (rng the Target of G2)
by XBOOLE_0:def 3;
then
{1,2} c= the
carrier of
G2
by A10, A20, ZFMISC_1:32;
then
{1,2} = the
carrier of
G2
by A21, XBOOLE_0:def 10;
then
the
carrier of
G1 c= the
carrier of
G2
by A12, XBOOLE_1:7;
hence
contradiction
by A6, XBOOLE_1:67;
verum end;
end;
thus
not G is void
; G is strict
thus
G is strict
; verum