set V = {1,2};
set E = {1};
A1:
1 in {1}
by TARSKI:def 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:57;
reconsider G = MultiGraphStruct(# {1,2},{1},S,T #) as Graph ;
A2:
( S . 1 = 1 & T . 1 = 2 )
by A1, FUNCOP_1:13;
take
G
; :: thesis: ( G is finite & G is simple & G is connected & not G is void & G is strict )
thus
G is finite
by GRAPH_1:def 9; :: thesis: ( G is simple & G is connected & not G is void & G is strict )
thus
G is simple
:: thesis: ( G is connected & not G is void & G is strict )
thus
G is connected
:: thesis: ( not G is void & G is strict )proof
given G1,
G2 being
Graph such that A4:
( the
carrier of
G1 misses the
carrier of
G2 &
G is_sum_of G1,
G2 )
;
:: according to GRAPH_1:def 8 :: thesis: contradiction
set MSG =
MultiGraphStruct(# the
carrier of
G,the
carrier' of
G,the
Source of
G,the
Target of
G #);
A5:
( the
Target of
G1 tolerates the
Target of
G2 & the
Source of
G1 tolerates the
Source of
G2 &
MultiGraphStruct(# the
carrier of
G,the
carrier' of
G,the
Source of
G,the
Target of
G #)
= G1 \/ G2 )
by A4, GRAPH_1:def 4;
then A6:
( 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 & 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 GRAPH_1:def 3;
set E1 = the
carrier' of
G1;
set E2 = the
carrier' of
G2;
set S1 = the
Source of
G1;
set S2 = the
Source of
G2;
set T1 = the
Target of
G1;
set T2 = the
Target of
G2;
set V1 = the
carrier of
G1;
set V2 = the
carrier of
G2;
A7:
(rng the Source of G1) \/ (rng the Target of G1) c= the
carrier of
G1
by Th3;
A8:
(rng the Source of G2) \/ (rng the Target of G2) c= the
carrier of
G2
by Th3;
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 A6, ZFMISC_1:43;
suppose A10:
( the
carrier' of
G1 = {1} & the
carrier' of
G2 = {} )
;
:: thesis: contradictionthen
( the
Source of
G1 . 1
= S . 1 & the
Target of
G1 . 1
= T . 1 )
by A1, A5, GRAPH_1:def 3;
then
( 1
in rng the
Source of
G1 & 2
in rng the
Target of
G1 )
by A1, A2, A10, FUNCT_2:6;
then
( 1
in (rng the Source of G1) \/ (rng the Target of G1) & 2
in (rng the Source of G1) \/ (rng the Target of G1) )
by XBOOLE_0:def 3;
then
(
{1,2} c= the
carrier of
G1 & the
carrier of
G1 c= {1,2} )
by A6, A7, XBOOLE_1:7, ZFMISC_1:38;
then
{1,2} = the
carrier of
G1
by XBOOLE_0:def 10;
then
( the
carrier of
G2 c= the
carrier of
G2 & the
carrier of
G2 c= the
carrier of
G1 )
by A6, XBOOLE_1:7;
hence
contradiction
by A4, XBOOLE_1:67;
:: thesis: verum end; suppose A11:
( the
carrier' of
G1 = {} & the
carrier' of
G2 = {1} )
;
:: thesis: contradictionthen
( the
Source of
G2 . 1
= S . 1 & the
Target of
G2 . 1
= T . 1 )
by A1, A5, GRAPH_1:def 3;
then
( 1
in rng the
Source of
G2 & 2
in rng the
Target of
G2 )
by A1, A2, A11, FUNCT_2:6;
then
( 1
in (rng the Source of G2) \/ (rng the Target of G2) & 2
in (rng the Source of G2) \/ (rng the Target of G2) )
by XBOOLE_0:def 3;
then
(
{1,2} c= the
carrier of
G2 & the
carrier of
G2 c= {1,2} )
by A6, A8, XBOOLE_1:7, ZFMISC_1:38;
then
{1,2} = the
carrier of
G2
by XBOOLE_0:def 10;
then
( the
carrier of
G1 c= the
carrier of
G1 & the
carrier of
G1 c= the
carrier of
G2 )
by A6, XBOOLE_1:7;
hence
contradiction
by A4, XBOOLE_1:67;
:: thesis: verum end;
end;
thus
not G is void
; :: thesis: G is strict
thus
G is strict
; :: thesis: verum