sgraph1.miz



    begin

    definition

      let m,n be Nat;

      :: SGRAPH1:def1

      func nat_interval (m,n) -> Subset of NAT equals { i where i be Nat : m <= i & i <= n };

      coherence

      proof

        set IT = { i where i be Nat : m <= i & i <= n };

        now

          let e be object;

          assume e in IT;

          then

          consider i be Nat such that

           A1: i = e and m <= i and

           A2: i <= n;

          now

            per cases ;

              suppose i = 0 ;

              then i in { 0 } by TARSKI:def 1;

              hence e in ( { 0 } \/ ( Seg n)) by A1, XBOOLE_0:def 3;

            end;

              suppose i <> 0 ;

              then ( 0 + 1) <= i by NAT_1: 13;

              then e in ( Seg n) by A1, A2;

              hence e in ( { 0 } \/ ( Seg n)) by XBOOLE_0:def 3;

            end;

          end;

          hence e in ( { 0 } \/ ( Seg n));

        end;

        then

         A3: IT c= ( { 0 } \/ ( Seg n));

         { 0 } c= NAT by ZFMISC_1: 31;

        then ( { 0 } \/ ( Seg n)) c= NAT by XBOOLE_1: 8;

        hence thesis by A3, XBOOLE_1: 1;

      end;

    end

    notation

      let m,n be Nat;

      synonym Seg (m,n) for nat_interval (m,n);

    end

    registration

      let m,n be Nat;

      cluster ( nat_interval (m,n)) -> finite;

      coherence

      proof

        set IT = { i where i be Nat : m <= i & i <= n };

        now

          let e be object;

          assume e in IT;

          then

          consider i be Nat such that

           A1: i = e and m <= i and

           A2: i <= n;

          now

            per cases ;

              suppose i = 0 ;

              then i in { 0 } by TARSKI:def 1;

              hence e in ( { 0 } \/ ( Seg n)) by A1, XBOOLE_0:def 3;

            end;

              suppose i <> 0 ;

              then ( 0 + 1) <= i by NAT_1: 13;

              then e in ( Seg n) by A1, A2;

              hence e in ( { 0 } \/ ( Seg n)) by XBOOLE_0:def 3;

            end;

          end;

          hence e in ( { 0 } \/ ( Seg n));

        end;

        then IT c= ( { 0 } \/ ( Seg n));

        hence thesis;

      end;

    end

    theorem :: SGRAPH1:1

    for m,n be Nat, e be set holds e in ( nat_interval (m,n)) iff ex i be Nat st e = i & m <= i & i <= n;

    theorem :: SGRAPH1:2

    for m,n,k be Nat holds k in ( nat_interval (m,n)) iff m <= k & k <= n

    proof

      let m,n,k be Nat;

      hereby

        assume k in ( nat_interval (m,n));

        then ex i be Nat st k = i & m <= i & i <= n;

        hence m <= k & k <= n;

      end;

      assume m <= k & k <= n;

      hence thesis;

    end;

    theorem :: SGRAPH1:3

    for n be Nat holds ( nat_interval (1,n)) = ( Seg n);

    theorem :: SGRAPH1:4

    

     Th4: for m,n be Nat st 1 <= m holds ( nat_interval (m,n)) c= ( Seg n)

    proof

      let m,n be Nat;

      assume

       A1: 1 <= m;

      now

        let e be object;

        assume e in ( nat_interval (m,n));

        then

        consider i be Nat such that

         A2: e = i and

         A3: m <= i and

         A4: i <= n;

        1 <= i by A1, A3, XXREAL_0: 2;

        hence e in ( Seg n) by A2, A4;

      end;

      hence thesis;

    end;

    theorem :: SGRAPH1:5

    

     Th5: for k,m,n be Nat st k < m holds ( Seg k) misses ( nat_interval (m,n))

    proof

      let k,m,n be Nat;

      assume

       A1: k < m;

      now

        let e be object;

        assume

         A2: e in (( Seg k) /\ ( nat_interval (m,n)));

        then e in ( nat_interval (m,n)) by XBOOLE_0:def 4;

        then

         A3: ex j be Nat st e = j & m <= j & j <= n;

        e in ( Seg k) by A2, XBOOLE_0:def 4;

        then ex i be Nat st e = i & 1 <= i & i <= k;

        hence e in {} by A1, A3, XXREAL_0: 2;

      end;

      then (( Seg k) /\ ( nat_interval (m,n))) c= {} ;

      then (( Seg k) /\ ( nat_interval (m,n))) = {} ;

      hence thesis by XBOOLE_0:def 7;

    end;

    theorem :: SGRAPH1:6

    for m,n be Nat st n < m holds ( nat_interval (m,n)) = {}

    proof

      let m,n be Nat;

      assume

       A1: n < m;

      now

        let e be object;

        assume e in ( nat_interval (m,n));

        then ex i be Nat st e = i & m <= i & i <= n;

        hence contradiction by A1, XXREAL_0: 2;

      end;

      hence thesis by XBOOLE_0:def 1;

    end;

    

     Lm1: for A be set, s be Subset of A, n be set st n in A holds (s \/ {n}) is Subset of A

    proof

      let A be set, s be Subset of A, n be set;

      assume

       A1: n in A;

      (s \/ {n}) c= A

      proof

        let m be object;

        assume

         A2: m in (s \/ {n});

        now

          per cases by A2, XBOOLE_0:def 3;

            suppose m in s;

            hence thesis;

          end;

            suppose m in {n};

            hence thesis by A1, TARSKI:def 1;

          end;

        end;

        hence thesis;

      end;

      hence thesis;

    end;

    definition

      let A be set;

      :: SGRAPH1:def2

      func TWOELEMENTSETS (A) -> set equals { z where z be Subset of A : ( card z) = 2 };

      coherence ;

    end

    theorem :: SGRAPH1:7

    

     Th7: for A,e be set holds e in ( TWOELEMENTSETS A) iff ex z be Subset of A st e = z & ( card z) = 2;

    theorem :: SGRAPH1:8

    

     Th8: for A,e be set holds (e in ( TWOELEMENTSETS A) iff (e is finite Subset of A & ex x,y be object st x in A & y in A & x <> y & e = {x, y}))

    proof

      let A,e be set;

      hereby

        assume e in ( TWOELEMENTSETS A);

        then

         A1: ex z be Subset of A st e = z & ( card z) = 2;

        then

        reconsider e9 = e as finite Subset of A;

        thus e is finite Subset of A by A1;

        consider x,y be object such that

         A2: x <> y and

         A3: e9 = {x, y} by A1, CARD_2: 60;

        take x, y;

        x in e9 & y in e9 by A3, TARSKI:def 2;

        hence x in A & y in A;

        thus x <> y & e = {x, y} by A2, A3;

      end;

      assume that e is finite Subset of A and

       A4: ex x,y be object st x in A & y in A & x <> y & e = {x, y};

      consider x,y be Element of A such that

       A5: x in A and y in A and

       A6: not x = y and

       A7: e = {x, y} by A4;

      reconsider xy = {x, y} as finite Subset of A by A5, ZFMISC_1: 32;

      ex z be finite Subset of A st e = z & ( card z) = 2

      proof

        take xy;

        thus e = xy by A7;

        thus thesis by A6, CARD_2: 57;

      end;

      hence thesis;

    end;

    theorem :: SGRAPH1:9

    

     Th9: for A be set holds ( TWOELEMENTSETS A) c= ( bool A)

    proof

      let A be set;

      let x be object;

      assume x in ( TWOELEMENTSETS A);

      then x is finite Subset of A by Th8;

      hence x in ( bool A);

    end;

    theorem :: SGRAPH1:10

    

     Th10: for A be set, e1,e2 be set st {e1, e2} in ( TWOELEMENTSETS A) holds e1 in A & e2 in A & e1 <> e2

    proof

      let A be set, e1,e2 be set;

      assume

       A1: {e1, e2} in ( TWOELEMENTSETS A);

      then

      consider x,y be object such that

       A2: x in A & y in A & not x = y and

       A3: {e1, e2} = {x, y} by Th8;

      per cases by A3, ZFMISC_1: 6;

        suppose e1 = x & e2 = x;

        then {x} in ( TWOELEMENTSETS A) by A1, ENUMSET1: 29;

        then ex x1,x2 be object st x1 in A & x2 in A & ( not x1 = x2) & {x} = {x1, x2} by Th8;

        hence thesis by ZFMISC_1: 5;

      end;

        suppose e1 = x & e2 = y;

        hence thesis by A2;

      end;

        suppose e1 = y & e2 = x;

        hence thesis by A2;

      end;

        suppose e1 = y & e2 = y;

        then {y} in ( TWOELEMENTSETS A) by A1, ENUMSET1: 29;

        then ex x1,x2 be object st x1 in A & x2 in A & ( not x1 = x2) & {y} = {x1, x2} by Th8;

        hence thesis by ZFMISC_1: 5;

      end;

    end;

    theorem :: SGRAPH1:11

    

     Th11: ( TWOELEMENTSETS {} ) = {}

    proof

      ( TWOELEMENTSETS {} ) c= {}

      proof

        let a be object;

        assume a in ( TWOELEMENTSETS {} );

        then ex a1,a2 be object st a1 in {} & a2 in {} & ( not a1 = a2) & a = {a1, a2} by Th8;

        hence thesis;

      end;

      hence thesis;

    end;

    registration

      cluster ( TWOELEMENTSETS {} ) -> empty;

      coherence by Th11;

    end

    theorem :: SGRAPH1:12

    for t,u be set st t c= u holds ( TWOELEMENTSETS t) c= ( TWOELEMENTSETS u)

    proof

      let t,u be set;

      assume

       A1: t c= u;

      let e be object;

      assume

       A2: e in ( TWOELEMENTSETS t);

      then e is finite Subset of t by Th8;

      then

       A3: e is finite Subset of u by A1, XBOOLE_1: 1;

      ex x,y be object st x in t & y in t & ( not x = y) & e = {x, y} by A2, Th8;

      hence thesis by A1, A3, Th8;

    end;

    ::$Canceled

    registration

      let A be finite set;

      cluster ( TWOELEMENTSETS A) -> finite;

      coherence by Th9, FINSET_1: 1;

    end

    registration

      let A be non trivial set;

      cluster ( TWOELEMENTSETS A) -> non empty;

      coherence

      proof

        consider a be object such that

         A1: a in A by XBOOLE_0:def 1;

        reconsider A9 = A as non empty non trivial set;

        consider b be object such that

         A2: b in (A9 \ {a}) by XBOOLE_0:def 1, ZFMISC_1: 139;

         not b in {a} by A2, XBOOLE_0:def 5;

        then

         A3: a <> b by TARSKI:def 1;

         {a, b} c= A by A1, A2, ZFMISC_1: 32;

        hence thesis by A1, A2, A3, Th8;

      end;

    end

    registration

      let a be set;

      cluster ( TWOELEMENTSETS {a}) -> empty;

      coherence

      proof

        now

          let x be object;

          assume x in ( TWOELEMENTSETS {a});

          then

          consider u,v be object such that

           A1: u in {a} and

           A2: v in {a} and

           A3: u <> v and x = {u, v} by Th8;

          u = a by A1, TARSKI:def 1

          .= v by A2, TARSKI:def 1;

          hence contradiction by A3;

        end;

        hence thesis by XBOOLE_0:def 1;

      end;

    end

    reserve X for set;

    begin

    definition

      struct ( 1-sorted) SimpleGraphStruct (# the carrier -> set,

the SEdges -> Subset of ( TWOELEMENTSETS the carrier) #)

       attr strict strict;

    end

    definition

      let X be set;

      :: SGRAPH1:def3

      func SIMPLEGRAPHS (X) -> set equals the set of all SimpleGraphStruct (# v, e #) where v be finite Subset of X, e be finite Subset of ( TWOELEMENTSETS v);

      coherence ;

    end

    theorem :: SGRAPH1:16

    

     Th16: SimpleGraphStruct (# {} , ( {} ( TWOELEMENTSETS {} )) #) in ( SIMPLEGRAPHS X)

    proof

      reconsider phiv = {} as finite Subset of X by XBOOLE_1: 2;

      reconsider phie = ( {} ( TWOELEMENTSETS {} )) as finite Subset of ( TWOELEMENTSETS phiv);

       SimpleGraphStruct (# phiv, phie #) in the set of all SimpleGraphStruct (# v, e #) where v be finite Subset of X, e be finite Subset of ( TWOELEMENTSETS v);

      hence thesis;

    end;

    registration

      let X be set;

      cluster ( SIMPLEGRAPHS X) -> non empty;

      coherence by Th16;

    end

    definition

      let X be set;

      :: SGRAPH1:def4

      mode SimpleGraph of X -> strict SimpleGraphStruct means

      : Def4: it is Element of ( SIMPLEGRAPHS X);

      existence

      proof

        take SimpleGraphStruct (# {} , ( {} ( TWOELEMENTSETS {} )) #);

        thus thesis by Th16;

      end;

    end

    theorem :: SGRAPH1:17

    

     Th17: for g be object holds (g in ( SIMPLEGRAPHS X) iff ex v be finite Subset of X, e be finite Subset of ( TWOELEMENTSETS v) st g = SimpleGraphStruct (# v, e #));

    begin

    theorem :: SGRAPH1:18

    

     Th18: for g be SimpleGraph of X holds the carrier of g c= X & the SEdges of g c= ( TWOELEMENTSETS the carrier of g)

    proof

      let g be SimpleGraph of X;

      g is Element of ( SIMPLEGRAPHS X) by Def4;

      then ex v be finite Subset of X, e be finite Subset of ( TWOELEMENTSETS v) st g = SimpleGraphStruct (# v, e #) by Th17;

      hence the carrier of g c= X;

      thus thesis;

    end;

    theorem :: SGRAPH1:19

    for g be SimpleGraph of X, e be set st e in the SEdges of g holds ex v1,v2 be object st v1 in the carrier of g & v2 in the carrier of g & v1 <> v2 & e = {v1, v2} by Th8;

    theorem :: SGRAPH1:20

    for g be SimpleGraph of X, v1,v2 be set st {v1, v2} in the SEdges of g holds v1 in the carrier of g & v2 in the carrier of g & v1 <> v2 by Th10;

    theorem :: SGRAPH1:21

    

     Th21: for g be SimpleGraph of X holds the carrier of g is finite Subset of X & the SEdges of g is finite Subset of ( TWOELEMENTSETS the carrier of g)

    proof

      let g be SimpleGraph of X;

      g is Element of ( SIMPLEGRAPHS X) by Def4;

      then ex v be finite Subset of X, e be finite Subset of ( TWOELEMENTSETS v) st g = SimpleGraphStruct (# v, e #) by Th17;

      hence thesis;

    end;

    definition

      let X;

      let G,G9 be SimpleGraph of X;

      :: SGRAPH1:def5

      pred G is_isomorphic_to G9 means ex Fv be Function of the carrier of G, the carrier of G9 st Fv is bijective & for v1,v2 be Element of G holds ( {v1, v2} in the SEdges of G iff {(Fv . v1), (Fv . v2)} in the SEdges of G);

    end

    begin

    scheme :: SGRAPH1:sch1

    IndSimpleGraphs0 { X() -> set , P[ set] } :

for G be set st G in ( SIMPLEGRAPHS X()) holds P[G]

      provided

       A1: P[ SimpleGraphStruct (# {} , ( {} ( TWOELEMENTSETS {} )) #)]

       and

       A2: for g be SimpleGraph of X(), v be set st g in ( SIMPLEGRAPHS X()) & P[g] & v in X() & not v in the carrier of g holds P[ SimpleGraphStruct (# (the carrier of g \/ {v}), ( {} ( TWOELEMENTSETS (the carrier of g \/ {v}))) #)]

       and

       A3: for g be SimpleGraph of X(), e be set st P[g] & e in ( TWOELEMENTSETS the carrier of g) & not e in the SEdges of g holds ex sege be Subset of ( TWOELEMENTSETS the carrier of g) st sege = (the SEdges of g \/ {e}) & P[ SimpleGraphStruct (# the carrier of g, sege #)];

      let g be set;

      assume

       A4: g in ( SIMPLEGRAPHS X());

      then

       A5: ex v be finite Subset of X(), e be finite Subset of ( TWOELEMENTSETS v) st g = SimpleGraphStruct (# v, e #);

      then

      reconsider G = g as SimpleGraph of X() by A4, Def4;

      

       A6: the carrier of G c= X() by Th18;

      per cases ;

        suppose

         A7: X() is empty;

        then the SEdges of G is Subset of {} by A6, Th11;

        hence thesis by A1, A6, A7;

      end;

        suppose not X() is empty;

        then

        reconsider X = X() as non empty set;

        defpred X[ set] means P[ SimpleGraphStruct (# $1, ( {} ( TWOELEMENTSETS $1)) #)];

         A8:

        now

          let B9 be Element of ( Fin X), b be Element of X;

          set g = SimpleGraphStruct (# B9, ( {} ( TWOELEMENTSETS B9)) #);

          B9 is finite Subset of X by FINSUB_1: 16;

          then

           A9: g in ( SIMPLEGRAPHS X());

          then

          reconsider g as SimpleGraph of X() by Def4;

          assume X[B9] & not b in B9;

          then P[ SimpleGraphStruct (# (the carrier of g \/ {b}), ( {} ( TWOELEMENTSETS (the carrier of g \/ {b}))) #)] by A2, A9;

          hence X[(B9 \/ {b})];

        end;

        

         A10: X[( {}. X)] by A1;

        

         A11: for VV be Element of ( Fin X) holds X[VV] from SETWISEO:sch 2( A10, A8);

         A12:

        now

          let VV be Element of ( Fin X);

          per cases ;

            suppose

             A13: ( TWOELEMENTSETS VV) = {} ;

            let EEa be Element of ( Fin ( TWOELEMENTSETS VV)), EE be Subset of ( TWOELEMENTSETS VV);

            assume EEa = EE;

            EE = ( {} ( TWOELEMENTSETS VV)) by A13;

            hence P[ SimpleGraphStruct (# VV, EE #)] by A11;

          end;

            suppose ( TWOELEMENTSETS VV) <> {} ;

            then

            reconsider TT = ( TWOELEMENTSETS VV) as non empty set;

            defpred Q[ Element of ( Fin TT)] means for EE be Subset of ( TWOELEMENTSETS VV) st EE = $1 holds P[ SimpleGraphStruct (# VV, EE #)];

             A14:

            now

              let ee be Element of ( Fin TT), vv be Element of TT such that

               A15: Q[ee] and

               A16: not vv in ee;

              reconsider ee9 = ee as Subset of ( TWOELEMENTSETS VV) by FINSUB_1: 16;

              set g = SimpleGraphStruct (# VV, ee9 #);

              VV is finite Subset of X() by FINSUB_1: 16;

              then g is Element of ( SIMPLEGRAPHS X()) by Th17;

              then

              reconsider g as SimpleGraph of X() by Def4;

              ex sege be Subset of ( TWOELEMENTSETS the carrier of g) st sege = (the SEdges of g \/ {vv}) & P[ SimpleGraphStruct (# the carrier of g, sege #)] by A3, A16, A15;

              hence Q[(ee \/ {.vv.})];

            end;

            

             A17: Q[( {}. TT)]

            proof

              let EE be Subset of ( TWOELEMENTSETS VV);

              assume EE = ( {}. TT);

              then EE = ( {} ( TWOELEMENTSETS VV));

              hence thesis by A11;

            end;

            for EE be Element of ( Fin TT) holds Q[EE] from SETWISEO:sch 2( A17, A14);

            hence for EE be Element of ( Fin ( TWOELEMENTSETS VV)), EE9 be Subset of ( TWOELEMENTSETS VV) st EE9 = EE holds P[ SimpleGraphStruct (# VV, EE9 #)];

          end;

        end;

        the carrier of G is Element of ( Fin X) & the SEdges of G is Element of ( Fin ( TWOELEMENTSETS the carrier of G)) by A5, FINSUB_1:def 5;

        hence thesis by A12;

      end;

    end;

    theorem :: SGRAPH1:22

    for g be SimpleGraph of X holds (g = SimpleGraphStruct (# {} , ( {} ( TWOELEMENTSETS {} )) #) or ex v be set, e be Subset of ( TWOELEMENTSETS v) st v is non empty & g = SimpleGraphStruct (# v, e #))

    proof

      let g be SimpleGraph of X;

      assume

       A1: not g = SimpleGraphStruct (# {} , ( {} ( TWOELEMENTSETS {} )) #);

      take the carrier of g, the SEdges of g;

      thus the carrier of g is non empty by A1;

      thus thesis;

    end;

    theorem :: SGRAPH1:23

    

     Th23: for V be Subset of X, E be Subset of ( TWOELEMENTSETS V), n be set, Evn be finite Subset of ( TWOELEMENTSETS (V \/ {n})) st SimpleGraphStruct (# V, E #) in ( SIMPLEGRAPHS X) & n in X holds SimpleGraphStruct (# (V \/ {n}), Evn #) in ( SIMPLEGRAPHS X)

    proof

      let V be Subset of X, E be Subset of ( TWOELEMENTSETS V), n be set, Evn be finite Subset of ( TWOELEMENTSETS (V \/ {n}));

      set g = SimpleGraphStruct (# V, E #);

      assume that

       A1: g in ( SIMPLEGRAPHS X) and

       A2: n in X;

      reconsider g as SimpleGraph of X by A1, Def4;

      V = the carrier of g;

      then V is finite Subset of X by Th21;

      then (V \/ {n}) is finite Subset of X by A2, Lm1;

      hence thesis;

    end;

    theorem :: SGRAPH1:24

    

     Th24: for V be Subset of X, E be Subset of ( TWOELEMENTSETS V), v1,v2 be set st v1 in V & v2 in V & v1 <> v2 & SimpleGraphStruct (# V, E #) in ( SIMPLEGRAPHS X) holds ex v1v2 be finite Subset of ( TWOELEMENTSETS V) st v1v2 = (E \/ { {v1, v2}}) & SimpleGraphStruct (# V, v1v2 #) in ( SIMPLEGRAPHS X)

    proof

      let V be Subset of X, E be Subset of ( TWOELEMENTSETS V), v1,v2 be set;

      set g = SimpleGraphStruct (# V, E #);

      assume that

       A1: v1 in V & v2 in V and

       A2: not v1 = v2 and

       A3: g in ( SIMPLEGRAPHS X);

      reconsider g as SimpleGraph of X by A3, Def4;

      

       A4: the SEdges of g is finite Subset of ( TWOELEMENTSETS V) by Th21;

      the carrier of g is finite Subset of X by Th21;

      then

      reconsider V as finite Subset of X;

      (E \/ { {v1, v2}}) c= ( TWOELEMENTSETS V) & (E \/ { {v1, v2}}) is finite

      proof

        hereby

          let e be object;

          assume

           A5: e in (E \/ { {v1, v2}});

          per cases by A5, XBOOLE_0:def 3;

            suppose e in E;

            hence e in ( TWOELEMENTSETS V);

          end;

            suppose e in { {v1, v2}};

            then

             A6: e = {v1, v2} by TARSKI:def 1;

            then e is Subset of V by A1, ZFMISC_1: 32;

            hence e in ( TWOELEMENTSETS V) by A1, A2, A6, Th8;

          end;

        end;

        thus thesis by A4;

      end;

      then

      reconsider E9 = (E \/ { {v1, v2}}) as finite Subset of ( TWOELEMENTSETS V);

       SimpleGraphStruct (# V, E9 #) in ( SIMPLEGRAPHS X);

      hence thesis;

    end;

    definition

      let X be set, GG be set;

      :: SGRAPH1:def6

      pred GG is_SetOfSimpleGraphs_of X means SimpleGraphStruct (# {} , ( {} ( TWOELEMENTSETS {} )) #) in GG & (for V be Subset of X, E be Subset of ( TWOELEMENTSETS V), n be set, Evn be finite Subset of ( TWOELEMENTSETS (V \/ {n})) st ( SimpleGraphStruct (# V, E #) in GG & n in X & not n in V) holds SimpleGraphStruct (# (V \/ {n}), Evn #) in GG) & for V be Subset of X, E be Subset of ( TWOELEMENTSETS V), v1,v2 be set st SimpleGraphStruct (# V, E #) in GG & v1 in V & v2 in V & v1 <> v2 & ( not {v1, v2} in E) holds ex v1v2 be finite Subset of ( TWOELEMENTSETS V) st v1v2 = (E \/ { {v1, v2}}) & SimpleGraphStruct (# V, v1v2 #) in GG;

    end

    theorem :: SGRAPH1:25

    

     Th25: ( SIMPLEGRAPHS X) is_SetOfSimpleGraphs_of X by Th16, Th23, Th24;

    theorem :: SGRAPH1:26

    

     Th26: for A be set st A is_SetOfSimpleGraphs_of X holds ( SIMPLEGRAPHS X) c= A

    proof

      let OTHER be set;

      defpred X[ set] means $1 in OTHER;

      assume

       A1: OTHER is_SetOfSimpleGraphs_of X;

      

       A2: for g be SimpleGraph of X, v be set st g in ( SIMPLEGRAPHS X) & X[g] & v in X & not v in the carrier of g holds X[ SimpleGraphStruct (# (the carrier of g \/ {v}), ( {} ( TWOELEMENTSETS (the carrier of g \/ {v}))) #)]

      proof

        let g be SimpleGraph of X, v be set;

        assume that g in ( SIMPLEGRAPHS X) and

         A3: g in OTHER & v in X & not v in the carrier of g;

        set SVg = the carrier of g;

        SVg is Subset of X by Th21;

        hence thesis by A1, A3;

      end;

      

       A4: for g be SimpleGraph of X, e be set st X[g] & e in ( TWOELEMENTSETS the carrier of g) & not e in the SEdges of g holds ex sege be Subset of ( TWOELEMENTSETS the carrier of g) st sege = (the SEdges of g \/ {e}) & X[ SimpleGraphStruct (# the carrier of g, sege #)]

      proof

        let g be SimpleGraph of X, e be set;

        assume that

         A5: g in OTHER and

         A6: e in ( TWOELEMENTSETS the carrier of g) and

         A7: not e in the SEdges of g;

        set SVg = the carrier of g, SEg = the SEdges of g;

        consider v1,v2 be object such that

         A8: v1 in SVg & v2 in SVg & v1 <> v2 and

         A9: e = {v1, v2} by A6, Th8;

        SVg is finite Subset of X by Th21;

        then

        consider v1v2 be finite Subset of ( TWOELEMENTSETS SVg) such that

         A10: v1v2 = (SEg \/ { {v1, v2}}) & SimpleGraphStruct (# SVg, v1v2 #) in OTHER by A1, A5, A7, A8, A9;

        take v1v2;

        thus thesis by A9, A10;

      end;

      let e be object;

      assume

       A11: e in ( SIMPLEGRAPHS X);

      

       A12: X[ SimpleGraphStruct (# {} , ( {} ( TWOELEMENTSETS {} )) #)] by A1;

      for e be set st e in ( SIMPLEGRAPHS X) holds X[e] from IndSimpleGraphs0( A12, A2, A4);

      hence thesis by A11;

    end;

    theorem :: SGRAPH1:27

    ( SIMPLEGRAPHS X) is_SetOfSimpleGraphs_of X & for A be set st A is_SetOfSimpleGraphs_of X holds ( SIMPLEGRAPHS X) c= A by Th25, Th26;

    begin

    definition

      let X be set, G be SimpleGraph of X;

      :: SGRAPH1:def7

      mode SubGraph of G -> SimpleGraph of X means the carrier of it c= the carrier of G & the SEdges of it c= the SEdges of G;

      existence ;

    end

    begin

    definition

      let X be set, G be SimpleGraph of X;

      let v be set;

      :: SGRAPH1:def8

      func degree (G,v) -> Element of NAT means

      : Def8: ex X be finite set st (for z be set holds (z in X iff z in the SEdges of G & v in z)) & it = ( card X);

      existence

      proof

        defpred X[ set] means v in $1;

        consider X be set such that

         A1: for z be set holds z in X iff z in the SEdges of G & X[z] from XFAMILY:sch 1;

        

         A2: X c= the SEdges of G by A1;

        the SEdges of G is finite by Th21;

        then

        reconsider X as finite set by A2;

        take ( card X), X;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let IT1,IT2 be Element of NAT ;

        assume (ex X1 be finite set st (for z be set holds (z in X1 iff z in the SEdges of G & v in z)) & IT1 = ( card X1)) & ex X2 be finite set st (for z be set holds (z in X2 iff z in the SEdges of G & v in z)) & IT2 = ( card X2);

        then

        consider X1,X2 be finite set such that

         A3: for z be set holds (z in X1 iff z in the SEdges of G & v in z) and

         A4: IT1 = ( card X1) and

         A5: for z be set holds (z in X2 iff z in the SEdges of G & v in z) and

         A6: IT2 = ( card X2);

        

         A7: X2 c= X1

        proof

          let z be object;

          reconsider zz = z as set by TARSKI: 1;

          assume z in X2;

          then z in the SEdges of G & v in zz by A5;

          hence thesis by A3;

        end;

        X1 c= X2

        proof

          let z be object;

          reconsider zz = z as set by TARSKI: 1;

          assume z in X1;

          then z in the SEdges of G & v in zz by A3;

          hence thesis by A5;

        end;

        hence thesis by A4, A6, A7, XBOOLE_0:def 10;

      end;

    end

    theorem :: SGRAPH1:28

    

     Th28: for X be non empty set, G be SimpleGraph of X, v be set holds ex ww be finite set st ww = { w where w be Element of X : w in the carrier of G & {v, w} in the SEdges of G } & ( degree (G,v)) = ( card ww)

    proof

      let X be non empty set, G be SimpleGraph of X, v be set;

      set ww = { w where w be Element of X : w in the carrier of G & {v, w} in the SEdges of G };

      consider Y be finite set such that

       A1: for z be set holds (z in Y iff z in the SEdges of G & v in z) and

       A2: ( degree (G,v)) = ( card Y) by Def8;

      

       A3: for z be set holds (z in ww iff z in the carrier of G & {v, z} in the SEdges of G)

      proof

        let z be set;

        hereby

          assume z in ww;

          then ex w be Element of X st z = w & w in the carrier of G & {v, w} in the SEdges of G;

          hence z in the carrier of G & {v, z} in the SEdges of G;

        end;

        thus z in the carrier of G & {v, z} in the SEdges of G implies z in ww

        proof

          assume

           A4: z in the carrier of G & {v, z} in the SEdges of G;

          the carrier of G is finite Subset of X by Th21;

          hence thesis by A4;

        end;

      end;

      

       A5: ww c= the carrier of G by A3;

      the carrier of G is finite by Th21;

      then

      reconsider ww as finite set by A5;

      take ww;

      (ww,Y) are_equipotent

      proof

        set wwY = { [w, {v, w}] where w be Element of X : w in ww & {v, w} in Y };

        take wwY;

        

         A6: for x,y,z,u be object st [x, y] in wwY & [z, u] in wwY holds (x = z iff y = u)

        proof

          let x,y,z,u be object;

          assume that

           A7: [x, y] in wwY and

           A8: [z, u] in wwY;

          consider w1 be Element of X such that

           A9: [x, y] = [w1, {v, w1}] and w1 in ww and

           A10: {v, w1} in Y by A7;

          consider w2 be Element of X such that

           A11: [z, u] = [w2, {v, w2}] and w2 in ww and {v, w2} in Y by A8;

          hereby

            assume

             A12: x = z;

            w1 = ( [w1, {v, w1}] `1 )

            .= ( [x, y] `1 ) by A9

            .= z by A12

            .= ( [w2, {v, w2}] `1 ) by A11

            .= w2;

            

            hence y = ( [w2, {v, w2}] `2 ) by A9

            .= u by A11;

          end;

          hereby

             {v, w1} in the SEdges of G by A1, A10;

            then

             A13: v <> w1 by Th10;

            assume

             A14: y = u;

             {v, w1} = ( [w1, {v, w1}] `2 )

            .= ( [x, y] `2 ) by A9

            .= u by A14

            .= ( [w2, {v, w2}] `2 ) by A11

            .= {v, w2};

            then w1 = w2 by A13, ZFMISC_1: 6;

            

            hence x = ( [z, u] `1 ) by A9, A11

            .= z;

          end;

        end;

        

         A15: for w be set holds ( [w, {v, w}] in wwY iff w in ww & {v, w} in Y)

        proof

          let w be set;

          hereby

            assume [w, {v, w}] in wwY;

            then

            consider w9 be Element of X such that

             A16: [w, {v, w}] = [w9, {v, w9}] and

             A17: w9 in ww & {v, w9} in Y;

            w = ( [w9, {v, w9}] `1 ) by A16

            .= w9;

            hence w in ww & {v, w} in Y by A17;

          end;

          thus w in ww & {v, w} in Y implies [w, {v, w}] in wwY

          proof

            assume that

             A18: w in ww and

             A19: {v, w} in Y;

            

             A20: w in the carrier of G by A3, A18;

            the carrier of G is finite Subset of X by Th21;

            then

            reconsider w as Element of X by A20;

            ex z be Element of X st [w, {v, w}] = [z, {v, z}] & z in ww & {v, z} in Y by A18, A19;

            hence thesis;

          end;

        end;

        

         A21: for y be object st y in Y holds ex x be object st x in ww & [x, y] in wwY

        proof

          let y be object;

          assume

           A22: y in Y;

          then

           A23: y in the SEdges of G by A1;

          reconsider yy = y as set by TARSKI: 1;

          

           A24: v in yy by A1, A22;

          ex w be set st w in the carrier of G & y = {v, w}

          proof

            consider v1,v2 be object such that

             A25: v1 in the carrier of G and

             A26: v2 in the carrier of G and v1 <> v2 and

             A27: y = {v1, v2} by A23, Th8;

            per cases by A24, A27, TARSKI:def 2;

              suppose

               A28: v = v1;

              take v2;

              thus thesis by A26, A27, A28;

            end;

              suppose

               A29: v = v2;

              take v1;

              thus thesis by A27, A29, A25;

            end;

          end;

          then

          consider w be set such that

           A30: w in the carrier of G and

           A31: y = {v, w};

          take w;

          thus w in ww by A3, A23, A30, A31;

          hence thesis by A15, A22, A31;

        end;

        for x be object st x in ww holds ex y be object st y in Y & [x, y] in wwY

        proof

          let x be object;

          assume

           A32: x in ww;

          take {v, x};

          

           A33: v in {v, x} by TARSKI:def 2;

           {v, x} in the SEdges of G by A3, A32;

          hence {v, x} in Y by A1, A33;

          hence thesis by A15, A32;

        end;

        hence thesis by A21, A6;

      end;

      hence thesis by A2, CARD_1: 5;

    end;

    theorem :: SGRAPH1:29

    for X be non empty set, g be SimpleGraph of X, v be set st v in the carrier of g holds ex VV be finite set st VV = the carrier of g & ( degree (g,v)) < ( card VV)

    proof

      let X be non empty set, g be SimpleGraph of X, v be set;

      reconsider VV = the carrier of g as finite set by Th21;

      consider ww be finite set such that

       A1: ww = { w where w be Element of X : w in VV & {v, w} in the SEdges of g } and

       A2: ( degree (g,v)) = ( card ww) by Th28;

      assume

       A3: v in the carrier of g;

       A4:

      now

        assume ww = VV;

        then

         A5: ex w be Element of X st v = w & w in VV & {v, w} in the SEdges of g by A3, A1;

         {v, v} = {v} by ENUMSET1: 29;

        then

        consider x,y be object such that x in VV and y in VV and

         A6: x <> y and

         A7: {v} = {x, y} by A5, Th8;

        v = x by A7, ZFMISC_1: 4;

        hence ww <> VV by A6, A7, ZFMISC_1: 4;

      end;

      take VV;

      ww c= VV

      proof

        let e be object;

        assume e in ww;

        then ex w be Element of X st e = w & w in VV & {v, w} in the SEdges of g by A1;

        hence thesis;

      end;

      then ww c< VV by A4, XBOOLE_0:def 8;

      hence thesis by A2, CARD_2: 48;

    end;

    theorem :: SGRAPH1:30

    for g be SimpleGraph of X, v,e be set st e in the SEdges of g & ( degree (g,v)) = 0 holds not v in e

    proof

      let g be SimpleGraph of X, v,e be set;

      assume that

       A1: e in the SEdges of g and

       A2: ( degree (g,v)) = 0 ;

      consider Y be finite set such that

       A3: for z be set holds (z in Y iff z in the SEdges of g & v in z) and

       A4: ( degree (g,v)) = ( card Y) by Def8;

      assume v in e;

      then Y is non empty by A1, A3;

      hence contradiction by A2, A4;

    end;

    theorem :: SGRAPH1:31

    for g be SimpleGraph of X, v be set, vg be finite set st vg = the carrier of g & v in vg & (1 + ( degree (g,v))) = ( card vg) holds for w be Element of vg st v <> w holds ex e be set st e in the SEdges of g & e = {v, w}

    proof

      let g be SimpleGraph of X, v be set, vg be finite set;

      assume that

       A1: vg = the carrier of g and

       A2: v in vg and

       A3: (1 + ( degree (g,v))) = ( card vg);

      vg is Subset of X by A1, Th21;

      then

      reconsider X as non empty set by A2;

      let w be Element of vg;

      assume

       A4: v <> w;

      take {v, w};

      hereby

        now

          consider ww be finite set such that

           A5: ww = { vv where vv be Element of X : vv in vg & {v, vv} in the SEdges of g } and

           A6: ( degree (g,v)) = ( card ww) by A1, Th28;

          reconsider wwv = (ww \/ {v}) as finite set;

          assume

           A7: not {v, w} in the SEdges of g;

          

           A8: not v in ww & not w in ww

          proof

            hereby

              assume v in ww;

              then ex vv be Element of X st v = vv & vv in vg & {v, vv} in the SEdges of g by A5;

              then {v} in the SEdges of g by ENUMSET1: 29;

              then ex z be Subset of vg st {v} = z & ( card z) = 2 by A1, Th7;

              hence contradiction by CARD_1: 30;

            end;

            assume w in ww;

            then ex vv be Element of X st w = vv & vv in vg & {v, vv} in the SEdges of g by A5;

            hence contradiction by A7;

          end;

           A9:

          now

            let e be object;

            assume e in ww;

            then ex vv be Element of X st e = vv & vv in vg & {v, vv} in the SEdges of g by A5;

            hence e in vg;

          end;

          wwv c= vg & wwv <> vg

          proof

            

             A10: {v} c= vg by A2, TARSKI:def 1;

            ww c= vg by A9;

            hence wwv c= vg by A10, XBOOLE_1: 8;

            assume

             A11: wwv = vg;

             not w in {v} by A4, TARSKI:def 1;

            hence contradiction by A8, A11, XBOOLE_0:def 3;

          end;

          then

           A12: wwv c< vg by XBOOLE_0:def 8;

          ( card wwv) = (1 + ( card ww)) by A8, CARD_2: 41;

          hence contradiction by A3, A6, A12, CARD_2: 48;

        end;

        hence {v, w} in the SEdges of g;

      end;

      thus thesis;

    end;

    begin

    definition

      let X be set, g be SimpleGraph of X, v1,v2 be Element of g, p be FinSequence of the carrier of g;

      :: SGRAPH1:def9

      pred p is_path_of v1,v2 means (p . 1) = v1 & (p . ( len p)) = v2 & (for i be Element of NAT st 1 <= i & i < ( len p) holds {(p . i), (p . (i + 1))} in the SEdges of g) & for i,j be Element of NAT st 1 <= i & i < ( len p) & i < j & j < ( len p) holds (p . i) <> (p . j) & {(p . i), (p . (i + 1))} <> {(p . j), (p . (j + 1))};

    end

    definition

      let X be set, g be SimpleGraph of X, v1,v2 be Element of the carrier of g;

      :: SGRAPH1:def10

      func PATHS (v1,v2) -> Subset of (the carrier of g * ) equals { ss where ss be Element of (the carrier of g * ) : ss is_path_of (v1,v2) };

      coherence

      proof

        set IT = { ss where ss be Element of (the carrier of g * ) : ss is_path_of (v1,v2) };

        IT c= (the carrier of g * )

        proof

          let e be object;

          assume e in IT;

          then ex ss be Element of (the carrier of g * ) st e = ss & ss is_path_of (v1,v2);

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: SGRAPH1:32

    for g be SimpleGraph of X, v1,v2 be Element of the carrier of g, e be set holds (e in ( PATHS (v1,v2)) iff ex ss be Element of (the carrier of g * ) st e = ss & ss is_path_of (v1,v2));

    theorem :: SGRAPH1:33

    for g be SimpleGraph of X, v1,v2 be Element of the carrier of g, e be Element of (the carrier of g * ) st e is_path_of (v1,v2) holds e in ( PATHS (v1,v2));

    definition

      let X be set, g be SimpleGraph of X, p be set;

      :: SGRAPH1:def11

      pred p is_cycle_of g means ex v be Element of the carrier of g st p in ( PATHS (v,v));

    end

    begin

    definition

      let n,m be Element of NAT ;

      :: SGRAPH1:def12

      func K_ (m,n) -> SimpleGraph of NAT means ex ee be Subset of ( TWOELEMENTSETS ( Seg (m + n))) st ee = { {i, j} where i,j be Element of NAT : i in ( Seg m) & j in ( nat_interval ((m + 1),(m + n))) } & it = SimpleGraphStruct (# ( Seg (m + n)), ee #);

      existence

      proof

        set VV = ( Seg (m + n)), V1 = ( Seg m), V2 = ( nat_interval ((m + 1),(m + n))), EE = { {i, j} where i,j be Element of NAT : i in V1 & j in V2 };

        

         A1: V1 c= VV by FINSEQ_1: 5, NAT_1: 11;

        

         A2: V2 c= VV by Th4, NAT_1: 11;

        EE c= ( TWOELEMENTSETS VV)

        proof

          let e be object;

          reconsider ee = e as set by TARSKI: 1;

          assume e in EE;

          then

          consider i0,j0 be Element of NAT such that

           A3: e = {i0, j0} and

           A4: i0 in V1 & j0 in V2;

          i0 in VV & j0 in VV by A1, A2, A4;

          then

           A5: ee c= VV by A3, TARSKI:def 2;

          m < (m + 1) by NAT_1: 13;

          then (V1 /\ V2) = {} by XBOOLE_0:def 7, Th5;

          then i0 <> j0 by A4, XBOOLE_0:def 4;

          hence thesis by A1, A2, A3, A4, A5, Th8;

        end;

        then

        reconsider EE as finite Subset of ( TWOELEMENTSETS VV);

        set IT = SimpleGraphStruct (# VV, EE #);

        IT in ( SIMPLEGRAPHS NAT );

        then

        reconsider IT as SimpleGraph of NAT by Def4;

        reconsider EE as Subset of ( TWOELEMENTSETS ( Seg (m + n)));

        take IT, EE;

        thus thesis;

      end;

      uniqueness ;

    end

    definition

      let n be Element of NAT ;

      :: SGRAPH1:def13

      func K_ (n) -> SimpleGraph of NAT means

      : Def13: ex ee be finite Subset of ( TWOELEMENTSETS ( Seg n)) st ee = { {i, j} where i,j be Element of NAT : i in ( Seg n) & j in ( Seg n) & i <> j } & it = SimpleGraphStruct (# ( Seg n), ee #);

      existence

      proof

        set EE = { {i, j} where i,j be Element of NAT : i in ( Seg n) & j in ( Seg n) & i <> j };

        now

          let e be object;

          reconsider ee = e as set by TARSKI: 1;

          assume e in EE;

          then

          consider i0,j0 be Element of NAT such that

           A1: e = {i0, j0} and

           A2: i0 in ( Seg n) and

           A3: j0 in ( Seg n) and

           A4: i0 <> j0;

          ee c= ( Seg n)

          proof

            let e0 be object;

            assume

             A5: e0 in ee;

            per cases by A1, A5, TARSKI:def 2;

              suppose e0 = i0;

              hence thesis by A2;

            end;

              suppose e0 = j0;

              hence thesis by A3;

            end;

          end;

          hence e in ( TWOELEMENTSETS ( Seg n)) by A1, A2, A3, A4, Th8;

        end;

        then EE c= ( TWOELEMENTSETS ( Seg n));

        then

        reconsider EE as finite Subset of ( TWOELEMENTSETS ( Seg n));

        set IT = SimpleGraphStruct (# ( Seg n), EE #);

        IT in ( SIMPLEGRAPHS NAT );

        then

        reconsider IT as SimpleGraph of NAT by Def4;

        take IT, EE;

        thus thesis;

      end;

      uniqueness ;

    end

    definition

      :: SGRAPH1:def14

      func TriangleGraph -> SimpleGraph of NAT equals ( K_ 3);

      correctness ;

    end

    theorem :: SGRAPH1:34

    

     Th34: ex ee be Subset of ( TWOELEMENTSETS ( Seg 3)) st ee = {. {.1, 2.}, {.2, 3.}, {.3, 1.}.} & TriangleGraph = SimpleGraphStruct (# ( Seg 3), ee #)

    proof

      consider ee be finite Subset of ( TWOELEMENTSETS ( Seg 3)) such that

       A1: ee = { {i, j} where i,j be Element of NAT : i in ( Seg 3) & j in ( Seg 3) & i <> j } and

       A2: TriangleGraph = SimpleGraphStruct (# ( Seg 3), ee #) by Def13;

      take ee;

      now

        let a be object;

        assume a in ee;

        then

        consider i,j be Element of NAT such that

         A3: a = {i, j} and

         A4: i in ( Seg 3) and

         A5: j in ( Seg 3) and

         A6: i <> j by A1;

        per cases by A4, ENUMSET1:def 1, FINSEQ_3: 1;

          suppose

           A7: i = 1;

          now

            per cases by A5, ENUMSET1:def 1, FINSEQ_3: 1;

              suppose j = 1;

              hence a in {. {.1, 2.}, {.2, 3.}, {.3, 1.}.} by A6, A7;

            end;

              suppose j = 2;

              hence a in {. {.1, 2.}, {.2, 3.}, {.3, 1.}.} by A3, A7, ENUMSET1:def 1;

            end;

              suppose j = 3;

              hence a in {. {.1, 2.}, {.2, 3.}, {.3, 1.}.} by A3, A7, ENUMSET1:def 1;

            end;

          end;

          hence a in {. {.1, 2.}, {.2, 3.}, {.3, 1.}.};

        end;

          suppose

           A8: i = 2;

          now

            per cases by A5, ENUMSET1:def 1, FINSEQ_3: 1;

              suppose j = 1;

              hence a in {. {.1, 2.}, {.2, 3.}, {.3, 1.}.} by A3, A8, ENUMSET1:def 1;

            end;

              suppose j = 2;

              hence a in {. {.1, 2.}, {.2, 3.}, {.3, 1.}.} by A6, A8;

            end;

              suppose j = 3;

              hence a in {. {.1, 2.}, {.2, 3.}, {.3, 1.}.} by A3, A8, ENUMSET1:def 1;

            end;

          end;

          hence a in {. {.1, 2.}, {.2, 3.}, {.3, 1.}.};

        end;

          suppose

           A9: i = 3;

          now

            per cases by A5, ENUMSET1:def 1, FINSEQ_3: 1;

              suppose j = 1;

              hence a in {. {.1, 2.}, {.2, 3.}, {.3, 1.}.} by A3, A9, ENUMSET1:def 1;

            end;

              suppose j = 2;

              hence a in {. {.1, 2.}, {.2, 3.}, {.3, 1.}.} by A3, A9, ENUMSET1:def 1;

            end;

              suppose j = 3;

              hence a in {. {.1, 2.}, {.2, 3.}, {.3, 1.}.} by A6, A9;

            end;

          end;

          hence a in {. {.1, 2.}, {.2, 3.}, {.3, 1.}.};

        end;

      end;

      then

       A10: ee c= {. {.1, 2.}, {.2, 3.}, {.3, 1.}.};

      now

        let e be object;

        assume

         A11: e in {. {.1, 2.}, {.2, 3.}, {.3, 1.}.};

        per cases by A11, ENUMSET1:def 1;

          suppose

           A12: e = {1, 2};

          now

            take i = 1, j = 2;

            thus e = {i, j} by A12;

            thus i in ( Seg 3) & j in ( Seg 3);

            thus i <> j;

          end;

          hence e in ee by A1;

        end;

          suppose

           A13: e = {2, 3};

          now

            take i = 2, j = 3;

            thus e = {i, j} & i in ( Seg 3) & j in ( Seg 3) & i <> j by A13;

          end;

          hence e in ee by A1;

        end;

          suppose

           A14: e = {3, 1};

          now

            take i = 3, j = 1;

            thus e = {i, j} & i in ( Seg 3) & j in ( Seg 3) & i <> j by A14;

          end;

          hence e in ee by A1;

        end;

      end;

      then {. {.1, 2.}, {.2, 3.}, {.3, 1.}.} c= ee;

      hence thesis by A2, A10, XBOOLE_0:def 10;

    end;

    theorem :: SGRAPH1:35

    the carrier of TriangleGraph = ( Seg 3) & the SEdges of TriangleGraph = {. {.1, 2.}, {.2, 3.}, {.3, 1.}.} by Th34;

    theorem :: SGRAPH1:36

     {1, 2} in the SEdges of TriangleGraph & {2, 3} in the SEdges of TriangleGraph & {3, 1} in the SEdges of TriangleGraph by Th34, ENUMSET1:def 1;

    theorem :: SGRAPH1:37

    ((( <*1*> ^ <*2*>) ^ <*3*>) ^ <*1*>) is_cycle_of TriangleGraph

    proof

      reconsider o = 1 as Element of the carrier of TriangleGraph by Th34, ENUMSET1:def 1, FINSEQ_3: 1;

      reconsider VERTICES = the carrier of TriangleGraph as non empty set by Th34;

      set p = ((( <*1*> ^ <*2*>) ^ <*3*>) ^ <*1*>);

      

       A1: (p . 1) = 1 by FINSEQ_1: 66;

      reconsider One = 1, Two = 2, Three = 3 as Element of VERTICES by Th34, ENUMSET1:def 1, FINSEQ_3: 1;

      

       A2: (p . 2) = 2 by FINSEQ_1: 66;

      reconsider ONE = <*One*>, TWO = <*Two*>, THREE = <*Three*> as FinSequence of the carrier of TriangleGraph ;

      p = (((ONE ^ TWO) ^ THREE) ^ ONE);

      then

      reconsider pp = p as Element of (the carrier of TriangleGraph * ) by FINSEQ_1:def 11;

      

       A3: (p . 3) = 3 by FINSEQ_1: 66;

      

       A4: (p . 4) = 1 by FINSEQ_1: 66;

       A5:

      now

        let i be Element of NAT ;

        assume that

         A6: 1 <= i and

         A7: i < ( len p);

        i < (3 + 1) by A7, FINSEQ_1: 66;

        then i <= 3 by NAT_1: 13;

        then

         A8: i in ( Seg 3) by A6;

        per cases by A8, ENUMSET1:def 1, FINSEQ_3: 1;

          suppose i = 1;

          hence {(pp . i), (pp . (i + 1))} in the SEdges of TriangleGraph by A1, A2, Th34, ENUMSET1:def 1;

        end;

          suppose i = 2;

          hence {(pp . i), (pp . (i + 1))} in the SEdges of TriangleGraph by A2, A3, Th34, ENUMSET1:def 1;

        end;

          suppose i = 3;

          hence {(pp . i), (pp . (i + 1))} in the SEdges of TriangleGraph by A3, A4, Th34, ENUMSET1:def 1;

        end;

      end;

       A9:

      now

        let i,j be Element of NAT ;

        assume that

         A10: 1 <= i and

         A11: i < ( len pp) and

         A12: i < j and

         A13: j < ( len pp);

        

         A14: (i + 1) <= j by A12, NAT_1: 13;

        i < (3 + 1) by A11, FINSEQ_1: 66;

        then i <= 3 by NAT_1: 13;

        then

         A15: i in ( Seg 3) by A10;

        

         A16: j < (3 + 1) by A13, FINSEQ_1: 66;

        then

         A17: j <= 3 by NAT_1: 13;

        per cases by A15, ENUMSET1:def 1, FINSEQ_3: 1;

          suppose

           A18: i = 1;

          then

           A19: (pp . i) = o by FINSEQ_1: 66;

          j = 2 or 2 < j & j <= 3 by A16, A14, A18, NAT_1: 13, XXREAL_0: 1;

          then

           A20: j = 2 or (2 + 1) <= j & j <= 3 by NAT_1: 13;

          now

            per cases by A20, XXREAL_0: 1;

              suppose

               A21: j = 2;

              hence (pp . i) <> (pp . j) by A19, FINSEQ_1: 66;

              thus {(pp . i), (pp . (i + 1))} <> {(pp . j), (pp . (j + 1))} by A1, A2, A3, A18, A21, ZFMISC_1: 6;

            end;

              suppose

               A22: j = 3;

              hence (pp . i) <> (pp . j) by A19, FINSEQ_1: 66;

              thus {(pp . i), (pp . (i + 1))} <> {(pp . j), (pp . (j + 1))} by A1, A2, A3, A18, A22, ZFMISC_1: 6;

            end;

          end;

          hence (pp . i) <> (pp . j) & {(pp . i), (pp . (i + 1))} <> {(pp . j), (pp . (j + 1))};

        end;

          suppose

           A23: i = 2;

          then j = 3 by A14, A17, XXREAL_0: 1;

          hence (pp . i) <> (pp . j) & {(pp . i), (pp . (i + 1))} <> {(pp . j), (pp . (j + 1))} by A2, A3, A4, A23, ZFMISC_1: 6;

        end;

          suppose i = 3;

          hence (pp . i) <> (pp . j) & {(pp . i), (pp . (i + 1))} <> {(pp . j), (pp . (j + 1))} by A12, A16, NAT_1: 13;

        end;

      end;

      pp is_path_of (o,o) by A4, A5, A9, FINSEQ_1: 66;

      then pp in ( PATHS (o,o));

      hence thesis;

    end;