:: GRAPH_3  semantic presentation begin  definitionlet "D" be    ($#m1_hidden :::"set"::: )  ; let "T" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_finseq_2 :::"FinSequenceSet"::: )   "of" (Set (Const "D")); let "S" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); :: original: :::"Element"::: redefine mode  :::"Element":::  "of" "S" ->    ($#m2_finseq_1 :::"FinSequence"::: )   "of" "D"; end; registrationlet "i", "j" be   ($#v1_abian :::"even"::: )    ($#m1_hidden :::"Integer":::); 
cluster (Set "i"  ($#k6_xcmplx_0 :::"-"::: )  "j") ->   ($#v1_abian :::"even"::: )   ; 
end; 
theorem :: GRAPH_3:1 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_hidden :::"Integer":::) "holds"   (Bool  "("  (Bool  "("  (Bool (Set (Var "i")) "is"   ($#v1_abian :::"even"::: )  ) "iff" (Bool (Set (Var "j")) "is"   ($#v1_abian :::"even"::: )  )  ")" ) "iff" (Bool (Set (Set (Var "i"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "j"))) "is"   ($#v1_abian :::"even"::: )  )  ")" )) ; 
 
theorem :: GRAPH_3:2 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"FinSequence":::)  (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "a")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set  "("  "(" (Set (Var "m")) "," (Set (Var "n")) ")"   ($#k1_graph_2 :::"-cut"::: )  (Set (Var "p")) ")" )))) "holds"  (Bool  "ex" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "p")))) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  "(" (Set (Var "m")) "," (Set (Var "n")) ")"   ($#k1_graph_2 :::"-cut"::: )  (Set (Var "p")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))) & (Bool (Set (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set (Var "m"))  ($#k2_nat_1 :::"+"::: )  (Set (Var "a")))) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))  ")" )))) ; 
 definitionlet "G" be   ($#l1_graph_1 :::"Graph":::); mode Vertex of "G" is    ($#m1_subset_1 :::"Element"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G"); end; 





























theorem :: GRAPH_3:3 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "c")) "being"    ($#m1_graph_1 :::"Chain"::: )   "of" (Set (Var "G"))  (Bool  "for" (Set (Var "vs")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))  "st" (Bool (Bool (Set (Var "vs"))  ($#r1_graph_2 :::"is_vertex_seq_of"::: )  (Set (Var "c")))) "holds"  (Bool  "not" (Bool (Set (Var "vs")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))))) ; 
 
theorem :: GRAPH_3:4 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "e")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "e"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G"))))) "holds"  (Bool (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "e")) ($#k9_finseq_1 :::"*>"::: ) ) "is"   ($#m2_graph_1 :::"Path":::) "of" (Set (Var "G"))))) ; 
 
theorem :: GRAPH_3:5 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m2_graph_1 :::"Path":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set  "(" (Set (Var "m")) "," (Set (Var "n")) ")"   ($#k2_graph_2 :::"-cut"::: )  (Set (Var "p"))) "is"   ($#m2_graph_1 :::"Path":::) "of" (Set (Var "G")))))) ; 
 
theorem :: GRAPH_3:6 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m2_graph_1 :::"Path":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "vs1")) "," (Set (Var "vs2")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))  "st" (Bool (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "p1")))  ($#r1_xboole_0 :::"misses"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "p2")))) & (Bool (Set (Var "vs1"))  ($#r1_graph_2 :::"is_vertex_seq_of"::: )  (Set (Var "p1"))) & (Bool (Set (Var "vs2"))  ($#r1_graph_2 :::"is_vertex_seq_of"::: )  (Set (Var "p2"))) & (Bool (Set (Set (Var "vs1"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "vs1")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "vs2"))  ($#k1_funct_1 :::"."::: )  (Num 1)))) "holds"  (Bool (Set (Set (Var "p1"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "p2"))) "is"   ($#m2_graph_1 :::"Path":::) "of" (Set (Var "G")))))) ; 
 
theorem :: GRAPH_3:7 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "c")) "being"    ($#m1_graph_1 :::"Chain"::: )   "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "c"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool (Set (Var "c")) "is"   ($#v1_msscyc_1 :::"cyclic"::: )  ))) ; 
 registrationlet "G" be   ($#l1_graph_1 :::"Graph":::); 
cluster   ($#v1_relat_1 :::"Relation-like"::: )   (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )   (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "G")  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v2_funct_1 :::"one-to-one"::: )     ($#v1_finset_1 :::"finite"::: )     ($#v1_finseq_1 :::"FinSequence-like"::: )     ($#v2_finseq_1 :::"FinSubsequence-like"::: )     ($#v1_msscyc_1 :::"cyclic"::: )    for    ($#m1_graph_1 :::"Chain"::: )   "of" "G"; 
end; 
theorem :: GRAPH_3:8 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "p")) "being"   ($#v1_msscyc_1 :::"cyclic"::: )    ($#m2_graph_1 :::"Path":::) "of" (Set (Var "G")) "holds"  (Bool (Set (Set  "("  "(" (Set  "(" (Set (Var "m"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "p")) ")" ) ")"   ($#k2_graph_2 :::"-cut"::: )  (Set (Var "p")) ")" )  ($#k8_finseq_1 :::"^"::: )  (Set  "("  "(" (Num 1) "," (Set (Var "m")) ")"   ($#k2_graph_2 :::"-cut"::: )  (Set (Var "p")) ")" )) "is"   ($#v1_msscyc_1 :::"cyclic"::: )    ($#m2_graph_1 :::"Path":::) "of" (Set (Var "G")))))) ; 
 
theorem :: GRAPH_3:9 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m2_graph_1 :::"Path":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Set (Var "m"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "p"))))) "holds"  (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "(" (Set  "("  "(" (Set  "(" (Set (Var "m"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "p")) ")" ) ")"   ($#k2_graph_2 :::"-cut"::: )  (Set (Var "p")) ")" )  ($#k8_finseq_1 :::"^"::: )  (Set  "("  "(" (Num 1) "," (Set (Var "m")) ")"   ($#k2_graph_2 :::"-cut"::: )  (Set (Var "p")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "p")))) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "(" (Set  "("  "(" (Set  "(" (Set (Var "m"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "p")) ")" ) ")"   ($#k2_graph_2 :::"-cut"::: )  (Set (Var "p")) ")" )  ($#k8_finseq_1 :::"^"::: )  (Set  "("  "(" (Num 1) "," (Set (Var "m")) ")"   ($#k2_graph_2 :::"-cut"::: )  (Set (Var "p")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "p")))) & (Bool (Set (Set  "(" (Set  "("  "(" (Set  "(" (Set (Var "m"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "p")) ")" ) ")"   ($#k2_graph_2 :::"-cut"::: )  (Set (Var "p")) ")" )  ($#k8_finseq_1 :::"^"::: )  (Set  "("  "(" (Num 1) "," (Set (Var "m")) ")"   ($#k2_graph_2 :::"-cut"::: )  (Set (Var "p")) ")" ) ")" )  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "m"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )))  ")" )))) ; 
 
theorem :: GRAPH_3:10 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "p")) "being"   ($#v1_msscyc_1 :::"cyclic"::: )    ($#m2_graph_1 :::"Path":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "p"))))) "holds"  (Bool  "ex" (Set (Var "p9")) "being"   ($#v1_msscyc_1 :::"cyclic"::: )    ($#m2_graph_1 :::"Path":::) "of" (Set (Var "G")) "st"  (Bool  "("  (Bool (Set (Set (Var "p9"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "p9")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "p")))) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "p9")))  ($#r1_hidden :::"="::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "p"))))  ")" ))))) ; 
 
theorem :: GRAPH_3:11 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "e")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "s")) "," (Set (Var "t")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "s"))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" (Set (Var "G")))  ($#k1_funct_1 :::"."::: )  (Set (Var "e")))) & (Bool (Set (Var "t"))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" (Set (Var "G")))  ($#k1_funct_1 :::"."::: )  (Set (Var "e"))))) "holds"  (Bool (Set  ($#k2_finseq_4 :::"<*"::: ) (Set (Var "t")) "," (Set (Var "s")) ($#k2_finseq_4 :::"*>"::: ) )  ($#r1_graph_2 :::"is_vertex_seq_of"::: )  (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "e")) ($#k9_finseq_1 :::"*>"::: ) ))))) ; 
 
theorem :: GRAPH_3:12 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "c")) "being"    ($#m1_graph_1 :::"Chain"::: )   "of" (Set (Var "G"))  (Bool  "for" (Set (Var "vs")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))  (Bool  "for" (Set (Var "e")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "e"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G")))) & (Bool (Set (Var "vs"))  ($#r1_graph_2 :::"is_vertex_seq_of"::: )  (Set (Var "c"))) & (Bool (Set (Set (Var "vs"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "vs")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" (Set (Var "G")))  ($#k1_funct_1 :::"."::: )  (Set (Var "e"))))) "holds"  (Bool  "("  (Bool (Set (Set (Var "c"))  ($#k7_finseq_1 :::"^"::: )  (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "e")) ($#k9_finseq_1 :::"*>"::: ) )) "is"    ($#m1_graph_1 :::"Chain"::: )   "of" (Set (Var "G"))) & (Bool  "ex" (Set (Var "vs9")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G"))) "st"  (Bool  "("  (Bool (Set (Var "vs9"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "vs"))  ($#k3_graph_2 :::"^'"::: )  (Set  ($#k10_finseq_1 :::"<*"::: ) (Set  "(" (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" (Set (Var "G")))  ($#k1_funct_1 :::"."::: )  (Set (Var "e")) ")" ) "," (Set  "(" (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" (Set (Var "G")))  ($#k1_funct_1 :::"."::: )  (Set (Var "e")) ")" ) ($#k10_finseq_1 :::"*>"::: ) ))) & (Bool (Set (Var "vs9"))  ($#r1_graph_2 :::"is_vertex_seq_of"::: )  (Set (Set (Var "c"))  ($#k7_finseq_1 :::"^"::: )  (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "e")) ($#k9_finseq_1 :::"*>"::: ) ))) & (Bool (Set (Set (Var "vs9"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set (Var "vs"))  ($#k1_funct_1 :::"."::: )  (Num 1))) & (Bool (Set (Set (Var "vs9"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "vs9")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" (Set (Var "G")))  ($#k1_funct_1 :::"."::: )  (Set (Var "e"))))  ")" ))  ")" ))))) ; 
 
theorem :: GRAPH_3:13 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "c")) "being"    ($#m1_graph_1 :::"Chain"::: )   "of" (Set (Var "G"))  (Bool  "for" (Set (Var "vs")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))  (Bool  "for" (Set (Var "e")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "e"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G")))) & (Bool (Set (Var "vs"))  ($#r1_graph_2 :::"is_vertex_seq_of"::: )  (Set (Var "c"))) & (Bool (Set (Set (Var "vs"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "vs")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" (Set (Var "G")))  ($#k1_funct_1 :::"."::: )  (Set (Var "e"))))) "holds"  (Bool  "("  (Bool (Set (Set (Var "c"))  ($#k7_finseq_1 :::"^"::: )  (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "e")) ($#k9_finseq_1 :::"*>"::: ) )) "is"    ($#m1_graph_1 :::"Chain"::: )   "of" (Set (Var "G"))) & (Bool  "ex" (Set (Var "vs9")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G"))) "st"  (Bool  "("  (Bool (Set (Var "vs9"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "vs"))  ($#k3_graph_2 :::"^'"::: )  (Set  ($#k10_finseq_1 :::"<*"::: ) (Set  "(" (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" (Set (Var "G")))  ($#k1_funct_1 :::"."::: )  (Set (Var "e")) ")" ) "," (Set  "(" (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" (Set (Var "G")))  ($#k1_funct_1 :::"."::: )  (Set (Var "e")) ")" ) ($#k10_finseq_1 :::"*>"::: ) ))) & (Bool (Set (Var "vs9"))  ($#r1_graph_2 :::"is_vertex_seq_of"::: )  (Set (Set (Var "c"))  ($#k7_finseq_1 :::"^"::: )  (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "e")) ($#k9_finseq_1 :::"*>"::: ) ))) & (Bool (Set (Set (Var "vs9"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set (Var "vs"))  ($#k1_funct_1 :::"."::: )  (Num 1))) & (Bool (Set (Set (Var "vs9"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "vs9")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" (Set (Var "G")))  ($#k1_funct_1 :::"."::: )  (Set (Var "e"))))  ")" ))  ")" ))))) ; 
 
theorem :: GRAPH_3:14 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "c")) "being"    ($#m1_graph_1 :::"Chain"::: )   "of" (Set (Var "G"))  (Bool  "for" (Set (Var "vs")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))  "st" (Bool (Bool (Set (Var "vs"))  ($#r1_graph_2 :::"is_vertex_seq_of"::: )  (Set (Var "c")))) "holds"  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "holds"  (Bool  "("   "not" (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "c")))) "or" (Bool  "("  (Bool (Set (Set (Var "vs"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" (Set (Var "G")))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "c"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")) ")" ))) & (Bool (Set (Set (Var "vs"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" (Set (Var "G")))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "c"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")) ")" )))  ")" ) "or" (Bool  "("  (Bool (Set (Set (Var "vs"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" (Set (Var "G")))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "c"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")) ")" ))) & (Bool (Set (Set (Var "vs"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" (Set (Var "G")))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "c"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")) ")" )))  ")" )  ")" ))))) ; 
 
theorem :: GRAPH_3:15 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "c")) "being"    ($#m1_graph_1 :::"Chain"::: )   "of" (Set (Var "G"))  (Bool  "for" (Set (Var "vs")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))  (Bool  "for" (Set (Var "e")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "vs"))  ($#r1_graph_2 :::"is_vertex_seq_of"::: )  (Set (Var "c"))) & (Bool (Set (Var "e"))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "c"))))) "holds"  (Bool  "("  (Bool (Set (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" (Set (Var "G")))  ($#k1_funct_1 :::"."::: )  (Set (Var "e")))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "vs")))) & (Bool (Set (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" (Set (Var "G")))  ($#k1_funct_1 :::"."::: )  (Set (Var "e")))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "vs"))))  ")" ))))) ; 
 definitionlet "G" be   ($#l1_graph_1 :::"Graph":::); let "X" be    ($#m1_hidden :::"set"::: )  ; :: original: :::"-VSet"::: redefine func "G" :::"-VSet"::: "X" ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G"); end; 
theorem :: GRAPH_3:16 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::) "holds"  (Bool (Set (Set (Var "G"))  ($#k1_graph_3 :::"-VSet"::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: GRAPH_3:17 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "e")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "e"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G")))) & (Bool (Set (Var "e"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool  "not" (Bool (Set (Set (Var "G"))  ($#k1_graph_3 :::"-VSet"::: )  (Set (Var "X"))) "is"   ($#v1_xboole_0 :::"empty"::: )  )))) ; 
 
theorem :: GRAPH_3:18 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::) "holds"   (Bool  "("  (Bool (Set (Var "G")) "is"   ($#v5_graph_1 :::"connected"::: )  ) "iff" (Bool  "for" (Set (Var "v1")) "," (Set (Var "v2")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "v1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "v2")))) "holds"  (Bool  "ex" (Set (Var "c")) "being"    ($#m1_graph_1 :::"Chain"::: )   "of" (Set (Var "G"))(Bool  "ex" (Set (Var "vs")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G"))) "st"  (Bool  "("  (Bool (Bool  "not" (Set (Var "c")) "is"   ($#v1_xboole_0 :::"empty"::: )  )) & (Bool (Set (Var "vs"))  ($#r1_graph_2 :::"is_vertex_seq_of"::: )  (Set (Var "c"))) & (Bool (Set (Set (Var "vs"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "v1"))) & (Bool (Set (Set (Var "vs"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "vs")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "v2")))  ")" ))))  ")" )) ; 
 
theorem :: GRAPH_3:19 (Bool  "for" (Set (Var "G")) "being"   ($#v5_graph_1 :::"connected"::: )    ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "X"))  ($#r1_xboole_0 :::"meets"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G")))) & (Bool (Bool  "not" (Set (Var "v"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "G"))  ($#k1_graph_3 :::"-VSet"::: )  (Set (Var "X")))))) "holds"  (Bool  "ex" (Set (Var "v9")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G"))(Bool  "ex" (Set (Var "e")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G"))) "st"  (Bool  "("  (Bool (Set (Var "v9"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "G"))  ($#k1_graph_3 :::"-VSet"::: )  (Set (Var "X")))) & (Bool (Bool  "not" (Set (Var "e"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) & (Bool  "("  (Bool (Set (Var "v9"))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" (Set (Var "G")))  ($#k1_funct_1 :::"."::: )  (Set (Var "e")))) "or" (Bool (Set (Var "v9"))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" (Set (Var "G")))  ($#k1_funct_1 :::"."::: )  (Set (Var "e"))))  ")" )  ")" )))))) ; 
 begin  definitionlet "G" be   ($#l1_graph_1 :::"Graph":::); let "v" be   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); let "X" be    ($#m1_hidden :::"set"::: )  ; func  :::"Edges_In":::  "(" "v" "," "X" ")"  ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "G") means :: GRAPH_3:def 1 (Bool  "for" (Set (Var "e")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "e"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "("  (Bool (Set (Var "e"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "G")) & (Bool (Set (Var "e"))  ($#r2_hidden :::"in"::: )  "X") & (Bool (Set (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" "G")  ($#k1_funct_1 :::"."::: )  (Set (Var "e")))  ($#r1_hidden :::"="::: )  "v")  ")" )  ")" )); func  :::"Edges_Out":::  "(" "v" "," "X" ")"  ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "G") means :: GRAPH_3:def 2 (Bool  "for" (Set (Var "e")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "e"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "("  (Bool (Set (Var "e"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "G")) & (Bool (Set (Var "e"))  ($#r2_hidden :::"in"::: )  "X") & (Bool (Set (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" "G")  ($#k1_funct_1 :::"."::: )  (Set (Var "e")))  ($#r1_hidden :::"="::: )  "v")  ")" )  ")" )); end; 














:: deftheorem    defines :::"Edges_In"::: GRAPH_3:def 1 :  (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b4")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G"))) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_graph_3 :::"Edges_In"::: )   "(" (Set (Var "v")) "," (Set (Var "X")) ")" )) "iff" (Bool  "for" (Set (Var "e")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "e"))  ($#r2_hidden :::"in"::: )  (Set (Var "b4"))) "iff" (Bool  "("  (Bool (Set (Var "e"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G")))) & (Bool (Set (Var "e"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" (Set (Var "G")))  ($#k1_funct_1 :::"."::: )  (Set (Var "e")))  ($#r1_hidden :::"="::: )  (Set (Var "v")))  ")" )  ")" ))  ")" ))))); 
 
:: deftheorem    defines :::"Edges_Out"::: GRAPH_3:def 2 :  (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b4")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G"))) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_graph_3 :::"Edges_Out"::: )   "(" (Set (Var "v")) "," (Set (Var "X")) ")" )) "iff" (Bool  "for" (Set (Var "e")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "e"))  ($#r2_hidden :::"in"::: )  (Set (Var "b4"))) "iff" (Bool  "("  (Bool (Set (Var "e"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G")))) & (Bool (Set (Var "e"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" (Set (Var "G")))  ($#k1_funct_1 :::"."::: )  (Set (Var "e")))  ($#r1_hidden :::"="::: )  (Set (Var "v")))  ")" )  ")" ))  ")" ))))); 
 definitionlet "G" be   ($#l1_graph_1 :::"Graph":::); let "v" be   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); let "X" be    ($#m1_hidden :::"set"::: )  ; func  :::"Edges_At":::  "(" "v" "," "X" ")"  ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "G") equals :: GRAPH_3:def 3 (Set (Set  "("  ($#k2_graph_3 :::"Edges_In"::: )   "(" "v" "," "X" ")"  ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k3_graph_3 :::"Edges_Out"::: )   "(" "v" "," "X" ")"  ")" )); end; 







:: deftheorem    defines :::"Edges_At"::: GRAPH_3:def 3 :  (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k4_graph_3 :::"Edges_At"::: )   "(" (Set (Var "v")) "," (Set (Var "X")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_graph_3 :::"Edges_In"::: )   "(" (Set (Var "v")) "," (Set (Var "X")) ")"  ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k3_graph_3 :::"Edges_Out"::: )   "(" (Set (Var "v")) "," (Set (Var "X")) ")"  ")" )))))); 
 registrationlet "G" be   ($#v6_graph_1 :::"finite"::: )    ($#l1_graph_1 :::"Graph":::); let "v" be   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); let "X" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k2_graph_3 :::"Edges_In"::: )   "(" "v" "," "X" ")" ) ->   ($#v1_finset_1 :::"finite"::: )   ; 

cluster (Set   ($#k3_graph_3 :::"Edges_Out"::: )   "(" "v" "," "X" ")" ) ->   ($#v1_finset_1 :::"finite"::: )   ; 

cluster (Set   ($#k4_graph_3 :::"Edges_At"::: )   "(" "v" "," "X" ")" ) ->   ($#v1_finset_1 :::"finite"::: )   ; 
end; registrationlet "G" be   ($#l1_graph_1 :::"Graph":::); let "v" be   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); let "X" be   ($#v1_xboole_0 :::"empty"::: )     ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k2_graph_3 :::"Edges_In"::: )   "(" "v" "," "X" ")" ) ->   ($#v1_xboole_0 :::"empty"::: )   ; 

cluster (Set   ($#k3_graph_3 :::"Edges_Out"::: )   "(" "v" "," "X" ")" ) ->   ($#v1_xboole_0 :::"empty"::: )   ; 

cluster (Set   ($#k4_graph_3 :::"Edges_At"::: )   "(" "v" "," "X" ")" ) ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; definitionlet "G" be   ($#l1_graph_1 :::"Graph":::); let "v" be   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); func  :::"Edges_In"::: "v" ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "G") equals :: GRAPH_3:def 4 (Set   ($#k2_graph_3 :::"Edges_In"::: )   "(" "v" "," (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "G") ")" ); func  :::"Edges_Out"::: "v" ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "G") equals :: GRAPH_3:def 5 (Set   ($#k3_graph_3 :::"Edges_Out"::: )   "(" "v" "," (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "G") ")" ); end; 












:: deftheorem    defines :::"Edges_In"::: GRAPH_3:def 4 :  (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds"  (Bool (Set   ($#k5_graph_3 :::"Edges_In"::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_graph_3 :::"Edges_In"::: )   "(" (Set (Var "v")) "," (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G"))) ")" )))); 
 
:: deftheorem    defines :::"Edges_Out"::: GRAPH_3:def 5 :  (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds"  (Bool (Set   ($#k6_graph_3 :::"Edges_Out"::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_graph_3 :::"Edges_Out"::: )   "(" (Set (Var "v")) "," (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G"))) ")" )))); 
 
theorem :: GRAPH_3:20 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k2_graph_3 :::"Edges_In"::: )   "(" (Set (Var "v")) "," (Set (Var "X")) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k5_graph_3 :::"Edges_In"::: )  (Set (Var "v"))))))) ; 
 
theorem :: GRAPH_3:21 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k3_graph_3 :::"Edges_Out"::: )   "(" (Set (Var "v")) "," (Set (Var "X")) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k6_graph_3 :::"Edges_Out"::: )  (Set (Var "v"))))))) ; 
 registrationlet "G" be   ($#v6_graph_1 :::"finite"::: )    ($#l1_graph_1 :::"Graph":::); let "v" be   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); 
cluster (Set   ($#k5_graph_3 :::"Edges_In"::: )  "v") ->   ($#v1_finset_1 :::"finite"::: )   ; 

cluster (Set   ($#k6_graph_3 :::"Edges_Out"::: )  "v") ->   ($#v1_finset_1 :::"finite"::: )   ; 
end; 
















theorem :: GRAPH_3:22 (Bool  "for" (Set (Var "G")) "being"   ($#v6_graph_1 :::"finite"::: )    ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k5_graph_3 :::"Edges_In"::: )  (Set (Var "v")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k8_graph_1 :::"EdgesIn"::: )  (Set (Var "v")))))) ; 
 
theorem :: GRAPH_3:23 (Bool  "for" (Set (Var "G")) "being"   ($#v6_graph_1 :::"finite"::: )    ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k6_graph_3 :::"Edges_Out"::: )  (Set (Var "v")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k9_graph_1 :::"EdgesOut"::: )  (Set (Var "v")))))) ; 
 definitionlet "G" be   ($#v6_graph_1 :::"finite"::: )    ($#l1_graph_1 :::"Graph":::); let "v" be   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); let "X" be    ($#m1_hidden :::"set"::: )  ; func  :::"Degree":::  "(" "v" "," "X" ")"  ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) equals :: GRAPH_3:def 6 (Set (Set  "("  ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k2_graph_3 :::"Edges_In"::: )   "(" "v" "," "X" ")"  ")" ) ")" )  ($#k2_nat_1 :::"+"::: )  (Set  "("  ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k3_graph_3 :::"Edges_Out"::: )   "(" "v" "," "X" ")"  ")" ) ")" )); end; 







:: deftheorem    defines :::"Degree"::: GRAPH_3:def 6 :  (Bool  "for" (Set (Var "G")) "being"   ($#v6_graph_1 :::"finite"::: )    ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k7_graph_3 :::"Degree"::: )   "(" (Set (Var "v")) "," (Set (Var "X")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k2_graph_3 :::"Edges_In"::: )   "(" (Set (Var "v")) "," (Set (Var "X")) ")"  ")" ) ")" )  ($#k2_nat_1 :::"+"::: )  (Set  "("  ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k3_graph_3 :::"Edges_Out"::: )   "(" (Set (Var "v")) "," (Set (Var "X")) ")"  ")" ) ")" )))))); 
 
theorem :: GRAPH_3:24 (Bool  "for" (Set (Var "G")) "being"   ($#v6_graph_1 :::"finite"::: )    ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds"  (Bool (Set   ($#k10_graph_1 :::"Degree"::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set   ($#k7_graph_3 :::"Degree"::: )   "(" (Set (Var "v")) "," (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G"))) ")" )))) ; 
 
theorem :: GRAPH_3:25 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "G")) "being"   ($#v6_graph_1 :::"finite"::: )    ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set   ($#k7_graph_3 :::"Degree"::: )   "(" (Set (Var "v")) "," (Set (Var "X")) ")" )  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "not" (Bool (Set   ($#k4_graph_3 :::"Edges_At"::: )   "(" (Set (Var "v")) "," (Set (Var "X")) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))))) ; 
 
theorem :: GRAPH_3:26 (Bool  "for" (Set (Var "e")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "G")) "being"   ($#v6_graph_1 :::"finite"::: )    ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "e"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G")))) & (Bool (Bool  "not" (Set (Var "e"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) & (Bool  "("  (Bool (Set (Var "v"))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" (Set (Var "G")))  ($#k1_funct_1 :::"."::: )  (Set (Var "e")))) "or" (Bool (Set (Var "v"))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" (Set (Var "G")))  ($#k1_funct_1 :::"."::: )  (Set (Var "e"))))  ")" )) "holds"  (Bool (Set   ($#k10_graph_1 :::"Degree"::: )  (Set (Var "v")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k7_graph_3 :::"Degree"::: )   "(" (Set (Var "v")) "," (Set (Var "X")) ")" ))))) ; 
 
theorem :: GRAPH_3:27 (Bool  "for" (Set (Var "G")) "being"   ($#v6_graph_1 :::"finite"::: )    ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "X2")) "," (Set (Var "X1")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X2"))  ($#r1_tarski :::"c="::: )  (Set (Var "X1")))) "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k2_graph_3 :::"Edges_In"::: )   "(" (Set (Var "v")) "," (Set  "(" (Set (Var "X1"))  ($#k6_subset_1 :::"\"::: )  (Set (Var "X2")) ")" ) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k2_graph_3 :::"Edges_In"::: )   "(" (Set (Var "v")) "," (Set (Var "X1")) ")"  ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k2_graph_3 :::"Edges_In"::: )   "(" (Set (Var "v")) "," (Set (Var "X2")) ")"  ")" ) ")" )))))) ; 
 
theorem :: GRAPH_3:28 (Bool  "for" (Set (Var "G")) "being"   ($#v6_graph_1 :::"finite"::: )    ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "X2")) "," (Set (Var "X1")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X2"))  ($#r1_tarski :::"c="::: )  (Set (Var "X1")))) "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k3_graph_3 :::"Edges_Out"::: )   "(" (Set (Var "v")) "," (Set  "(" (Set (Var "X1"))  ($#k6_subset_1 :::"\"::: )  (Set (Var "X2")) ")" ) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k3_graph_3 :::"Edges_Out"::: )   "(" (Set (Var "v")) "," (Set (Var "X1")) ")"  ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k3_graph_3 :::"Edges_Out"::: )   "(" (Set (Var "v")) "," (Set (Var "X2")) ")"  ")" ) ")" )))))) ; 
 
theorem :: GRAPH_3:29 (Bool  "for" (Set (Var "G")) "being"   ($#v6_graph_1 :::"finite"::: )    ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "X2")) "," (Set (Var "X1")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X2"))  ($#r1_tarski :::"c="::: )  (Set (Var "X1")))) "holds"  (Bool (Set   ($#k7_graph_3 :::"Degree"::: )   "(" (Set (Var "v")) "," (Set  "(" (Set (Var "X1"))  ($#k6_subset_1 :::"\"::: )  (Set (Var "X2")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k7_graph_3 :::"Degree"::: )   "(" (Set (Var "v")) "," (Set (Var "X1")) ")"  ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k7_graph_3 :::"Degree"::: )   "(" (Set (Var "v")) "," (Set (Var "X2")) ")"  ")" )))))) ; 
 
theorem :: GRAPH_3:30 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "G")) "being"   ($#v6_graph_1 :::"finite"::: )    ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds"   (Bool  "("  (Bool (Set   ($#k2_graph_3 :::"Edges_In"::: )   "(" (Set (Var "v")) "," (Set (Var "X")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k2_graph_3 :::"Edges_In"::: )   "(" (Set (Var "v")) "," (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G"))) ")" ) ")" )) & (Bool (Set   ($#k3_graph_3 :::"Edges_Out"::: )   "(" (Set (Var "v")) "," (Set (Var "X")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_graph_3 :::"Edges_Out"::: )   "(" (Set (Var "v")) "," (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G"))) ")" ) ")" ))  ")" )))) ; 
 
theorem :: GRAPH_3:31 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "G")) "being"   ($#v6_graph_1 :::"finite"::: )    ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds"  (Bool (Set   ($#k7_graph_3 :::"Degree"::: )   "(" (Set (Var "v")) "," (Set (Var "X")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k7_graph_3 :::"Degree"::: )   "(" (Set (Var "v")) "," (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G"))) ")" ) ")" ))))) ; 
 
theorem :: GRAPH_3:32 (Bool  "for" (Set (Var "G")) "being"   ($#v6_graph_1 :::"finite"::: )    ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "c")) "being"    ($#m1_graph_1 :::"Chain"::: )   "of" (Set (Var "G"))  (Bool  "for" (Set (Var "vs")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))  "st" (Bool (Bool (Bool  "not" (Set (Var "c")) "is"   ($#v1_xboole_0 :::"empty"::: )  )) & (Bool (Set (Var "vs"))  ($#r1_graph_2 :::"is_vertex_seq_of"::: )  (Set (Var "c")))) "holds"  (Bool  "("  (Bool (Set (Var "v"))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "vs")))) "iff" (Bool (Set   ($#k7_graph_3 :::"Degree"::: )   "(" (Set (Var "v")) "," (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "c")) ")" ) ")" )  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ))))) ; 
 
theorem :: GRAPH_3:33 (Bool  "for" (Set (Var "G")) "being"  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#v5_graph_1 :::"connected"::: )     ($#v6_graph_1 :::"finite"::: )    ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G"))  "holds" (Bool (Set   ($#k10_graph_1 :::"Degree"::: )  (Set (Var "v")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 begin  definitionlet "G" be   ($#l1_graph_1 :::"Graph":::); let "v1", "v2" be   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); func  :::"AddNewEdge":::  "(" "v1" "," "v2" ")"  ->   ($#v1_graph_1 :::"strict"::: )    ($#l1_graph_1 :::"Graph":::) means :: GRAPH_3:def 7 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G")) & (Bool (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "G")  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "G") ($#k1_tarski :::"}"::: ) ))) & (Bool (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" "G")  ($#k1_funct_4 :::"+*"::: )  (Set  "(" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "G")  ($#k16_funcop_1 :::".-->"::: )  "v1" ")" ))) & (Bool (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" "G")  ($#k1_funct_4 :::"+*"::: )  (Set  "(" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "G")  ($#k16_funcop_1 :::".-->"::: )  "v2" ")" )))  ")" ); end; 







:: deftheorem    defines :::"AddNewEdge"::: GRAPH_3:def 7 :  (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v1")) "," (Set (Var "v2")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "b4")) "being"   ($#v1_graph_1 :::"strict"::: )    ($#l1_graph_1 :::"Graph":::) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_graph_3 :::"AddNewEdge"::: )   "(" (Set (Var "v1")) "," (Set (Var "v2")) ")" )) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b4")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))) & (Bool (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "b4")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G")))  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G"))) ($#k1_tarski :::"}"::: ) ))) & (Bool (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" (Set (Var "b4")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" (Set (Var "G")))  ($#k1_funct_4 :::"+*"::: )  (Set  "(" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G")))  ($#k16_funcop_1 :::".-->"::: )  (Set (Var "v1")) ")" ))) & (Bool (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" (Set (Var "b4")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" (Set (Var "G")))  ($#k1_funct_4 :::"+*"::: )  (Set  "(" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G")))  ($#k16_funcop_1 :::".-->"::: )  (Set (Var "v2")) ")" )))  ")" )  ")" )))); 
 registrationlet "G" be   ($#v6_graph_1 :::"finite"::: )    ($#l1_graph_1 :::"Graph":::); let "v1", "v2" be   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); 
cluster (Set   ($#k8_graph_3 :::"AddNewEdge"::: )   "(" "v1" "," "v2" ")" ) ->   ($#v1_graph_1 :::"strict"::: )     ($#v6_graph_1 :::"finite"::: )   ; 
end; 


























theorem :: GRAPH_3:34 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v1")) "," (Set (Var "v2")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds"   (Bool  "("  (Bool (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G")))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set  "("  ($#k8_graph_3 :::"AddNewEdge"::: )   "(" (Set (Var "v1")) "," (Set (Var "v2")) ")"  ")" ))) & (Bool (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set  "("  ($#k8_graph_3 :::"AddNewEdge"::: )   "(" (Set (Var "v1")) "," (Set (Var "v2")) ")"  ")" ))  ($#k6_subset_1 :::"\"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G"))) ($#k1_tarski :::"}"::: ) ))) & (Bool (Set (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" (Set  "("  ($#k8_graph_3 :::"AddNewEdge"::: )   "(" (Set (Var "v1")) "," (Set (Var "v2")) ")"  ")" ))  ($#k1_funct_1 :::"."::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G"))))  ($#r1_hidden :::"="::: )  (Set (Var "v1"))) & (Bool (Set (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" (Set  "("  ($#k8_graph_3 :::"AddNewEdge"::: )   "(" (Set (Var "v1")) "," (Set (Var "v2")) ")"  ")" ))  ($#k1_funct_1 :::"."::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G"))))  ($#r1_hidden :::"="::: )  (Set (Var "v2")))  ")" ))) ; 
 
theorem :: GRAPH_3:35 (Bool  "for" (Set (Var "e")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v1")) "," (Set (Var "v2")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "e"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G"))))) "holds"  (Bool  "("  (Bool (Set (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" (Set  "("  ($#k8_graph_3 :::"AddNewEdge"::: )   "(" (Set (Var "v1")) "," (Set (Var "v2")) ")"  ")" ))  ($#k1_funct_1 :::"."::: )  (Set (Var "e")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" (Set (Var "G")))  ($#k1_funct_1 :::"."::: )  (Set (Var "e")))) & (Bool (Set (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" (Set  "("  ($#k8_graph_3 :::"AddNewEdge"::: )   "(" (Set (Var "v1")) "," (Set (Var "v2")) ")"  ")" ))  ($#k1_funct_1 :::"."::: )  (Set (Var "e")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" (Set (Var "G")))  ($#k1_funct_1 :::"."::: )  (Set (Var "e"))))  ")" )))) ; 
 
theorem :: GRAPH_3:36 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v1")) "," (Set (Var "v2")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "c")) "being"    ($#m1_graph_1 :::"Chain"::: )   "of" (Set (Var "G"))  (Bool  "for" (Set (Var "vs")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))  (Bool  "for" (Set (Var "vs9")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k8_graph_3 :::"AddNewEdge"::: )   "(" (Set (Var "v1")) "," (Set (Var "v2")) ")"  ")" ))  "st" (Bool (Bool (Set (Var "vs9"))  ($#r1_hidden :::"="::: )  (Set (Var "vs"))) & (Bool (Set (Var "vs"))  ($#r1_graph_2 :::"is_vertex_seq_of"::: )  (Set (Var "c")))) "holds"  (Bool (Set (Var "vs9"))  ($#r1_graph_2 :::"is_vertex_seq_of"::: )  (Set (Var "c")))))))) ; 
 
theorem :: GRAPH_3:37 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v1")) "," (Set (Var "v2")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "c")) "being"    ($#m1_graph_1 :::"Chain"::: )   "of" (Set (Var "G")) "holds"  (Bool (Set (Var "c")) "is"    ($#m1_graph_1 :::"Chain"::: )   "of" (Set   ($#k8_graph_3 :::"AddNewEdge"::: )   "(" (Set (Var "v1")) "," (Set (Var "v2")) ")" ))))) ; 
 
theorem :: GRAPH_3:38 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v1")) "," (Set (Var "v2")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "p")) "being"   ($#m2_graph_1 :::"Path":::) "of" (Set (Var "G")) "holds"  (Bool (Set (Var "p")) "is"   ($#m2_graph_1 :::"Path":::) "of" (Set   ($#k8_graph_3 :::"AddNewEdge"::: )   "(" (Set (Var "v1")) "," (Set (Var "v2")) ")" ))))) ; 
 
theorem :: GRAPH_3:39 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v1")) "," (Set (Var "v2")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "v9")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set  "("  ($#k8_graph_3 :::"AddNewEdge"::: )   "(" (Set (Var "v1")) "," (Set (Var "v2")) ")"  ")" )  "st" (Bool (Bool (Set (Var "v9"))  ($#r1_hidden :::"="::: )  (Set (Var "v1"))) & (Bool (Set (Var "v1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "v2")))) "holds"  (Bool (Set   ($#k2_graph_3 :::"Edges_In"::: )   "(" (Set (Var "v9")) "," (Set (Var "X")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k2_graph_3 :::"Edges_In"::: )   "(" (Set (Var "v1")) "," (Set (Var "X")) ")" )))))) ; 
 
theorem :: GRAPH_3:40 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v2")) "," (Set (Var "v1")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "v9")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set  "("  ($#k8_graph_3 :::"AddNewEdge"::: )   "(" (Set (Var "v1")) "," (Set (Var "v2")) ")"  ")" )  "st" (Bool (Bool (Set (Var "v9"))  ($#r1_hidden :::"="::: )  (Set (Var "v2"))) & (Bool (Set (Var "v1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "v2")))) "holds"  (Bool (Set   ($#k3_graph_3 :::"Edges_Out"::: )   "(" (Set (Var "v9")) "," (Set (Var "X")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_graph_3 :::"Edges_Out"::: )   "(" (Set (Var "v2")) "," (Set (Var "X")) ")" )))))) ; 
 
theorem :: GRAPH_3:41 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v2")) "," (Set (Var "v1")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "v9")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set  "("  ($#k8_graph_3 :::"AddNewEdge"::: )   "(" (Set (Var "v1")) "," (Set (Var "v2")) ")"  ")" )  "st" (Bool (Bool (Set (Var "v9"))  ($#r1_hidden :::"="::: )  (Set (Var "v1"))) & (Bool (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G")))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool  "("  (Bool (Set   ($#k3_graph_3 :::"Edges_Out"::: )   "(" (Set (Var "v9")) "," (Set (Var "X")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_graph_3 :::"Edges_Out"::: )   "(" (Set (Var "v1")) "," (Set (Var "X")) ")"  ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G"))) ($#k1_tarski :::"}"::: ) ))) & (Bool (Set   ($#k3_graph_3 :::"Edges_Out"::: )   "(" (Set (Var "v1")) "," (Set (Var "X")) ")" )  ($#r1_xboole_0 :::"misses"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G"))) ($#k1_tarski :::"}"::: ) ))  ")" ))))) ; 
 
theorem :: GRAPH_3:42 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v1")) "," (Set (Var "v2")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "v9")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set  "("  ($#k8_graph_3 :::"AddNewEdge"::: )   "(" (Set (Var "v1")) "," (Set (Var "v2")) ")"  ")" )  "st" (Bool (Bool (Set (Var "v9"))  ($#r1_hidden :::"="::: )  (Set (Var "v2"))) & (Bool (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G")))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool  "("  (Bool (Set   ($#k2_graph_3 :::"Edges_In"::: )   "(" (Set (Var "v9")) "," (Set (Var "X")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_graph_3 :::"Edges_In"::: )   "(" (Set (Var "v2")) "," (Set (Var "X")) ")"  ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G"))) ($#k1_tarski :::"}"::: ) ))) & (Bool (Set   ($#k2_graph_3 :::"Edges_In"::: )   "(" (Set (Var "v2")) "," (Set (Var "X")) ")" )  ($#r1_xboole_0 :::"misses"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G"))) ($#k1_tarski :::"}"::: ) ))  ")" ))))) ; 
 
theorem :: GRAPH_3:43 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v1")) "," (Set (Var "v")) "," (Set (Var "v2")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "v9")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set  "("  ($#k8_graph_3 :::"AddNewEdge"::: )   "(" (Set (Var "v1")) "," (Set (Var "v2")) ")"  ")" )  "st" (Bool (Bool (Set (Var "v9"))  ($#r1_hidden :::"="::: )  (Set (Var "v"))) & (Bool (Set (Var "v"))  ($#r1_hidden :::"<>"::: )  (Set (Var "v2")))) "holds"  (Bool (Set   ($#k2_graph_3 :::"Edges_In"::: )   "(" (Set (Var "v9")) "," (Set (Var "X")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k2_graph_3 :::"Edges_In"::: )   "(" (Set (Var "v")) "," (Set (Var "X")) ")" )))))) ; 
 
theorem :: GRAPH_3:44 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v2")) "," (Set (Var "v")) "," (Set (Var "v1")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "v9")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set  "("  ($#k8_graph_3 :::"AddNewEdge"::: )   "(" (Set (Var "v1")) "," (Set (Var "v2")) ")"  ")" )  "st" (Bool (Bool (Set (Var "v9"))  ($#r1_hidden :::"="::: )  (Set (Var "v"))) & (Bool (Set (Var "v"))  ($#r1_hidden :::"<>"::: )  (Set (Var "v1")))) "holds"  (Bool (Set   ($#k3_graph_3 :::"Edges_Out"::: )   "(" (Set (Var "v9")) "," (Set (Var "X")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_graph_3 :::"Edges_Out"::: )   "(" (Set (Var "v")) "," (Set (Var "X")) ")" )))))) ; 
 
theorem :: GRAPH_3:45 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v1")) "," (Set (Var "v2")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "p9")) "being"   ($#m2_graph_1 :::"Path":::) "of" (Set   ($#k8_graph_3 :::"AddNewEdge"::: )   "(" (Set (Var "v1")) "," (Set (Var "v2")) ")" )  "st" (Bool (Bool (Bool  "not" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G")))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "p9")))))) "holds"  (Bool (Set (Var "p9")) "is"   ($#m2_graph_1 :::"Path":::) "of" (Set (Var "G")))))) ; 
 
theorem :: GRAPH_3:46 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v1")) "," (Set (Var "v2")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "vs")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))  (Bool  "for" (Set (Var "p9")) "being"   ($#m2_graph_1 :::"Path":::) "of" (Set   ($#k8_graph_3 :::"AddNewEdge"::: )   "(" (Set (Var "v1")) "," (Set (Var "v2")) ")" )  (Bool  "for" (Set (Var "vs9")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k8_graph_3 :::"AddNewEdge"::: )   "(" (Set (Var "v1")) "," (Set (Var "v2")) ")"  ")" ))  "st" (Bool (Bool (Bool  "not" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G")))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "p9"))))) & (Bool (Set (Var "vs"))  ($#r1_hidden :::"="::: )  (Set (Var "vs9"))) & (Bool (Set (Var "vs9"))  ($#r1_graph_2 :::"is_vertex_seq_of"::: )  (Set (Var "p9")))) "holds"  (Bool (Set (Var "vs"))  ($#r1_graph_2 :::"is_vertex_seq_of"::: )  (Set (Var "p9")))))))) ; 
 registrationlet "G" be   ($#v5_graph_1 :::"connected"::: )    ($#l1_graph_1 :::"Graph":::); let "v1", "v2" be   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); 
cluster (Set   ($#k8_graph_3 :::"AddNewEdge"::: )   "(" "v1" "," "v2" ")" ) ->   ($#v1_graph_1 :::"strict"::: )     ($#v5_graph_1 :::"connected"::: )   ; 
end; 














theorem :: GRAPH_3:47 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "G")) "being"   ($#v6_graph_1 :::"finite"::: )    ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "v2")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "v9")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set  "("  ($#k8_graph_3 :::"AddNewEdge"::: )   "(" (Set (Var "v1")) "," (Set (Var "v2")) ")"  ")" )  "st" (Bool (Bool (Set (Var "v9"))  ($#r1_hidden :::"="::: )  (Set (Var "v"))) & (Bool (Set (Var "v1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "v2"))) & (Bool  "("  (Bool (Set (Var "v"))  ($#r1_hidden :::"="::: )  (Set (Var "v1"))) "or" (Bool (Set (Var "v"))  ($#r1_hidden :::"="::: )  (Set (Var "v2")))  ")" ) & (Bool (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G")))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set   ($#k7_graph_3 :::"Degree"::: )   "(" (Set (Var "v9")) "," (Set (Var "X")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k7_graph_3 :::"Degree"::: )   "(" (Set (Var "v")) "," (Set (Var "X")) ")"  ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1))))))) ; 
 
theorem :: GRAPH_3:48 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "G")) "being"   ($#v6_graph_1 :::"finite"::: )    ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "v2")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "v9")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set  "("  ($#k8_graph_3 :::"AddNewEdge"::: )   "(" (Set (Var "v1")) "," (Set (Var "v2")) ")"  ")" )  "st" (Bool (Bool (Set (Var "v9"))  ($#r1_hidden :::"="::: )  (Set (Var "v"))) & (Bool (Set (Var "v"))  ($#r1_hidden :::"<>"::: )  (Set (Var "v1"))) & (Bool (Set (Var "v"))  ($#r1_hidden :::"<>"::: )  (Set (Var "v2")))) "holds"  (Bool (Set   ($#k7_graph_3 :::"Degree"::: )   "(" (Set (Var "v9")) "," (Set (Var "X")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k7_graph_3 :::"Degree"::: )   "(" (Set (Var "v")) "," (Set (Var "X")) ")" )))))) ; 
 begin  
theorem :: GRAPH_3:49 (Bool  "for" (Set (Var "G")) "being"   ($#v6_graph_1 :::"finite"::: )    ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "c")) "being"   ($#v1_msscyc_1 :::"cyclic"::: )    ($#m2_graph_1 :::"Path":::) "of" (Set (Var "G")) "holds"  (Bool (Set   ($#k7_graph_3 :::"Degree"::: )   "(" (Set (Var "v")) "," (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "c")) ")" ) ")" ) "is"   ($#v1_abian :::"even"::: )  )))) ; 
 
theorem :: GRAPH_3:50 (Bool  "for" (Set (Var "G")) "being"   ($#v6_graph_1 :::"finite"::: )    ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "vs")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))  (Bool  "for" (Set (Var "c")) "being"   ($#m2_graph_1 :::"Path":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Bool  "not" (Set (Var "c")) "is"   ($#v1_msscyc_1 :::"cyclic"::: )  )) & (Bool (Set (Var "vs"))  ($#r1_graph_2 :::"is_vertex_seq_of"::: )  (Set (Var "c")))) "holds"  (Bool  "("  (Bool (Set   ($#k7_graph_3 :::"Degree"::: )   "(" (Set (Var "v")) "," (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "c")) ")" ) ")" ) "is"   ($#v1_abian :::"even"::: )  ) "iff" (Bool  "("  (Bool (Set (Var "v"))  ($#r1_hidden :::"<>"::: )  (Set (Set (Var "vs"))  ($#k1_funct_1 :::"."::: )  (Num 1))) & (Bool (Set (Var "v"))  ($#r1_hidden :::"<>"::: )  (Set (Set (Var "vs"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "vs")) ")" )))  ")" )  ")" ))))) ; 
 








definitionlet "G" be   ($#l1_graph_1 :::"Graph":::); func "G" :::"-CycleSet":::  ->    ($#m1_finseq_2 :::"FinSequenceSet"::: )   "of" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "G") means :: GRAPH_3:def 8 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool (Set (Var "x")) "is"   ($#v1_msscyc_1 :::"cyclic"::: )    ($#m2_graph_1 :::"Path":::) "of" "G")  ")" )); end; 





:: deftheorem    defines :::"-CycleSet"::: GRAPH_3:def 8 :  (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "b2")) "being"    ($#m1_finseq_2 :::"FinSequenceSet"::: )   "of" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G"))) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "G"))  ($#k9_graph_3 :::"-CycleSet"::: )  )) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b2"))) "iff" (Bool (Set (Var "x")) "is"   ($#v1_msscyc_1 :::"cyclic"::: )    ($#m2_graph_1 :::"Path":::) "of" (Set (Var "G")))  ")" ))  ")" ))); 
 
theorem :: GRAPH_3:51 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::) "holds"  (Bool (Set   ($#k1_xboole_0 :::"{}"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Set (Var "G"))  ($#k9_graph_3 :::"-CycleSet"::: )  ))) ; 
 registrationlet "G" be   ($#l1_graph_1 :::"Graph":::); 
cluster (Set "G"  ($#k9_graph_3 :::"-CycleSet"::: )  ) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; 
theorem :: GRAPH_3:52 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "c")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set (Set (Var "G"))  ($#k9_graph_3 :::"-CycleSet"::: )  )  "st" (Bool (Bool (Set (Var "v"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "G"))  ($#k1_graph_3 :::"-VSet"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "c")) ")" )))) "holds"  (Bool  "{"  (Set (Var "c9")) where c9 "is"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set (Set (Var "G"))  ($#k9_graph_3 :::"-CycleSet"::: )  ) : (Bool  "("  (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "c9")))  ($#r1_hidden :::"="::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "c")))) & (Bool  "ex" (Set (Var "vs")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G"))) "st"  (Bool  "("  (Bool (Set (Var "vs"))  ($#r1_graph_2 :::"is_vertex_seq_of"::: )  (Set (Var "c9"))) & (Bool (Set (Set (Var "vs"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "v")))  ")" ))  ")" )  "}"   "is"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set (Var "G"))  ($#k9_graph_3 :::"-CycleSet"::: )  ")" ))))) ; 
 definitionlet "G" be   ($#l1_graph_1 :::"Graph":::); let "v" be   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); let "c" be    ($#m2_finseq_2 :::"Element"::: )   "of" (Set (Set (Const "G"))  ($#k9_graph_3 :::"-CycleSet"::: )  ); assume 
(Bool (Set (Const "v"))  ($#r2_hidden :::"in"::: )  (Set (Set (Const "G"))  ($#k1_graph_3 :::"-VSet"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Const "c")) ")" )))
 ; func  :::"Rotate":::  "(" "c" "," "v" ")"  ->    ($#m2_finseq_2 :::"Element"::: )   "of" (Set "G"  ($#k9_graph_3 :::"-CycleSet"::: )  ) equals :: GRAPH_3:def 9 (Set   ($#k10_subset_1 :::"choose"::: )   "{"  (Set (Var "c9")) where c9 "is"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set "G"  ($#k9_graph_3 :::"-CycleSet"::: )  ) : (Bool  "("  (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "c9")))  ($#r1_hidden :::"="::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  "c")) & (Bool  "ex" (Set (Var "vs")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G") "st"  (Bool  "("  (Bool (Set (Var "vs"))  ($#r1_graph_2 :::"is_vertex_seq_of"::: )  (Set (Var "c9"))) & (Bool (Set (Set (Var "vs"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  "v")  ")" ))  ")" )  "}"  ); end; 








:: deftheorem    defines :::"Rotate"::: GRAPH_3:def 9 :  (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "c")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set (Set (Var "G"))  ($#k9_graph_3 :::"-CycleSet"::: )  )  "st" (Bool (Bool (Set (Var "v"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "G"))  ($#k1_graph_3 :::"-VSet"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "c")) ")" )))) "holds"  (Bool (Set   ($#k10_graph_3 :::"Rotate"::: )   "(" (Set (Var "c")) "," (Set (Var "v")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k10_subset_1 :::"choose"::: )   "{"  (Set (Var "c9")) where c9 "is"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set (Set (Var "G"))  ($#k9_graph_3 :::"-CycleSet"::: )  ) : (Bool  "("  (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "c9")))  ($#r1_hidden :::"="::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "c")))) & (Bool  "ex" (Set (Var "vs")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G"))) "st"  (Bool  "("  (Bool (Set (Var "vs"))  ($#r1_graph_2 :::"is_vertex_seq_of"::: )  (Set (Var "c9"))) & (Bool (Set (Set (Var "vs"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "v")))  ")" ))  ")" )  "}"  ))))); 
 definitionlet "G" be   ($#l1_graph_1 :::"Graph":::); let "c1", "c2" be    ($#m2_finseq_2 :::"Element"::: )   "of" (Set (Set (Const "G"))  ($#k9_graph_3 :::"-CycleSet"::: )  ); assume that  
(Bool (Set (Set (Const "G"))  ($#k1_graph_3 :::"-VSet"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Const "c1")) ")" ))  ($#r1_xboole_0 :::"meets"::: )  (Set (Set (Const "G"))  ($#k1_graph_3 :::"-VSet"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Const "c2")) ")" )))
 and  
(Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Const "c1")))  ($#r1_xboole_0 :::"misses"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Const "c2"))))
 ; func  :::"CatCycles":::  "(" "c1" "," "c2" ")"  ->    ($#m2_finseq_2 :::"Element"::: )   "of" (Set "G"  ($#k9_graph_3 :::"-CycleSet"::: )  ) means :: GRAPH_3:def 10 (Bool  "ex" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" "G" "st"  (Bool  "("  (Bool (Set (Var "v"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_subset_1 :::"choose"::: )  (Set  "(" (Set  "(" "G"  ($#k1_graph_3 :::"-VSet"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  "c1" ")" ) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "(" "G"  ($#k1_graph_3 :::"-VSet"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  "c2" ")" ) ")" ) ")" ))) & (Bool it  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k10_graph_3 :::"Rotate"::: )   "(" "c1" "," (Set (Var "v")) ")"  ")" )  ($#k8_finseq_1 :::"^"::: )  (Set  "("  ($#k10_graph_3 :::"Rotate"::: )   "(" "c2" "," (Set (Var "v")) ")"  ")" )))  ")" )); end; 








:: deftheorem    defines :::"CatCycles"::: GRAPH_3:def 10 :  (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "c1")) "," (Set (Var "c2")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set (Set (Var "G"))  ($#k9_graph_3 :::"-CycleSet"::: )  )  "st" (Bool (Bool (Set (Set (Var "G"))  ($#k1_graph_3 :::"-VSet"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "c1")) ")" ))  ($#r1_xboole_0 :::"meets"::: )  (Set (Set (Var "G"))  ($#k1_graph_3 :::"-VSet"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "c2")) ")" ))) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "c1")))  ($#r1_xboole_0 :::"misses"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "c2"))))) "holds"  (Bool  "for" (Set (Var "b4")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set (Set (Var "G"))  ($#k9_graph_3 :::"-CycleSet"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k11_graph_3 :::"CatCycles"::: )   "(" (Set (Var "c1")) "," (Set (Var "c2")) ")" )) "iff" (Bool  "ex" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st"  (Bool  "("  (Bool (Set (Var "v"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_subset_1 :::"choose"::: )  (Set  "(" (Set  "(" (Set (Var "G"))  ($#k1_graph_3 :::"-VSet"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "c1")) ")" ) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "(" (Set (Var "G"))  ($#k1_graph_3 :::"-VSet"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "c2")) ")" ) ")" ) ")" ))) & (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k10_graph_3 :::"Rotate"::: )   "(" (Set (Var "c1")) "," (Set (Var "v")) ")"  ")" )  ($#k8_finseq_1 :::"^"::: )  (Set  "("  ($#k10_graph_3 :::"Rotate"::: )   "(" (Set (Var "c2")) "," (Set (Var "v")) ")"  ")" )))  ")" ))  ")" )))); 
 
theorem :: GRAPH_3:53 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "c1")) "," (Set (Var "c2")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set (Set (Var "G"))  ($#k9_graph_3 :::"-CycleSet"::: )  )  "st" (Bool (Bool (Set (Set (Var "G"))  ($#k1_graph_3 :::"-VSet"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "c1")) ")" ))  ($#r1_xboole_0 :::"meets"::: )  (Set (Set (Var "G"))  ($#k1_graph_3 :::"-VSet"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "c2")) ")" ))) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "c1")))  ($#r1_xboole_0 :::"misses"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "c2")))) & (Bool  "("  (Bool (Set (Var "c1"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) "or" (Bool (Set (Var "c2"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" )) "holds"  (Bool  "not" (Bool (Set   ($#k11_graph_3 :::"CatCycles"::: )   "(" (Set (Var "c1")) "," (Set (Var "c2")) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  )))) ; 
 








definitionlet "G" be   ($#v6_graph_1 :::"finite"::: )    ($#l1_graph_1 :::"Graph":::); let "v" be   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); let "X" be    ($#m1_hidden :::"set"::: )  ; assume 
(Bool (Set   ($#k7_graph_3 :::"Degree"::: )   "(" (Set (Const "v")) "," (Set (Const "X")) ")" )  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))
 ; func "X" :::"-PathSet"::: "v" ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_finseq_2 :::"FinSequenceSet"::: )   "of" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "G") equals :: GRAPH_3:def 11  "{"  (Set (Var "c")) where c "is"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set "X"  ($#k3_finseq_2 :::"*"::: )  ) : (Bool  "("  (Bool (Set (Var "c")) "is"   ($#m2_graph_1 :::"Path":::) "of" "G") & (Bool (Bool  "not" (Set (Var "c")) "is"   ($#v1_xboole_0 :::"empty"::: )  )) & (Bool  "ex" (Set (Var "vs")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G") "st"  (Bool  "("  (Bool (Set (Var "vs"))  ($#r1_graph_2 :::"is_vertex_seq_of"::: )  (Set (Var "c"))) & (Bool (Set (Set (Var "vs"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  "v")  ")" ))  ")" )  "}"  ; end; 








:: deftheorem    defines :::"-PathSet"::: GRAPH_3:def 11 :  (Bool  "for" (Set (Var "G")) "being"   ($#v6_graph_1 :::"finite"::: )    ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k7_graph_3 :::"Degree"::: )   "(" (Set (Var "v")) "," (Set (Var "X")) ")" )  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "X"))  ($#k12_graph_3 :::"-PathSet"::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "c")) where c "is"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set (Set (Var "X"))  ($#k3_finseq_2 :::"*"::: )  ) : (Bool  "("  (Bool (Set (Var "c")) "is"   ($#m2_graph_1 :::"Path":::) "of" (Set (Var "G"))) & (Bool (Bool  "not" (Set (Var "c")) "is"   ($#v1_xboole_0 :::"empty"::: )  )) & (Bool  "ex" (Set (Var "vs")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G"))) "st"  (Bool  "("  (Bool (Set (Var "vs"))  ($#r1_graph_2 :::"is_vertex_seq_of"::: )  (Set (Var "c"))) & (Bool (Set (Set (Var "vs"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "v")))  ")" ))  ")" )  "}"  )))); 
 
theorem :: GRAPH_3:54 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "G")) "being"   ($#v6_graph_1 :::"finite"::: )    ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "p")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set (Set (Var "X"))  ($#k12_graph_3 :::"-PathSet"::: )  (Set (Var "v")))  (Bool  "for" (Set (Var "Y")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "Y"))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G")))) & (Bool (Set   ($#k7_graph_3 :::"Degree"::: )   "(" (Set (Var "v")) "," (Set (Var "X")) ")" )  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "p")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "Y"))))))))) ; 
 definitionlet "G" be   ($#v6_graph_1 :::"finite"::: )    ($#l1_graph_1 :::"Graph":::); let "v" be   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); let "X" be    ($#m1_hidden :::"set"::: )  ; assume that  
(Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")) "holds"  (Bool (Set   ($#k7_graph_3 :::"Degree"::: )   "(" (Set (Var "v")) "," (Set (Const "X")) ")" ) "is"   ($#v1_abian :::"even"::: )  ))
 and  
(Bool (Set   ($#k7_graph_3 :::"Degree"::: )   "(" (Set (Const "v")) "," (Set (Const "X")) ")" )  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))
 ; func "X" :::"-CycleSet"::: "v" ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" "G"  ($#k9_graph_3 :::"-CycleSet"::: )  ")" ) equals :: GRAPH_3:def 12  "{"  (Set (Var "c")) where c "is"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set "G"  ($#k9_graph_3 :::"-CycleSet"::: )  ) : (Bool  "("  (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "c")))  ($#r1_tarski :::"c="::: )  "X") & (Bool (Bool  "not" (Set (Var "c")) "is"   ($#v1_xboole_0 :::"empty"::: )  )) & (Bool  "ex" (Set (Var "vs")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G") "st"  (Bool  "("  (Bool (Set (Var "vs"))  ($#r1_graph_2 :::"is_vertex_seq_of"::: )  (Set (Var "c"))) & (Bool (Set (Set (Var "vs"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  "v")  ")" ))  ")" )  "}"  ; end; 








:: deftheorem    defines :::"-CycleSet"::: GRAPH_3:def 12 :  (Bool  "for" (Set (Var "G")) "being"   ($#v6_graph_1 :::"finite"::: )    ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds"  (Bool (Set   ($#k7_graph_3 :::"Degree"::: )   "(" (Set (Var "v")) "," (Set (Var "X")) ")" ) "is"   ($#v1_abian :::"even"::: )  )  ")" ) & (Bool (Set   ($#k7_graph_3 :::"Degree"::: )   "(" (Set (Var "v")) "," (Set (Var "X")) ")" )  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "X"))  ($#k13_graph_3 :::"-CycleSet"::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "c")) where c "is"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set (Set (Var "G"))  ($#k9_graph_3 :::"-CycleSet"::: )  ) : (Bool  "("  (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "c")))  ($#r1_tarski :::"c="::: )  (Set (Var "X"))) & (Bool (Bool  "not" (Set (Var "c")) "is"   ($#v1_xboole_0 :::"empty"::: )  )) & (Bool  "ex" (Set (Var "vs")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G"))) "st"  (Bool  "("  (Bool (Set (Var "vs"))  ($#r1_graph_2 :::"is_vertex_seq_of"::: )  (Set (Var "c"))) & (Bool (Set (Set (Var "vs"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "v")))  ")" ))  ")" )  "}"  )))); 
 
theorem :: GRAPH_3:55 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "G")) "being"   ($#v6_graph_1 :::"finite"::: )    ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set   ($#k7_graph_3 :::"Degree"::: )   "(" (Set (Var "v")) "," (Set (Var "X")) ")" )  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool  "("   "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds"  (Bool (Set   ($#k7_graph_3 :::"Degree"::: )   "(" (Set (Var "v")) "," (Set (Var "X")) ")" ) "is"   ($#v1_abian :::"even"::: )  )  ")" )) "holds"  (Bool  "for" (Set (Var "c")) "being"    ($#m1_graph_3 :::"Element"::: )   "of" (Set (Set (Var "X"))  ($#k13_graph_3 :::"-CycleSet"::: )  (Set (Var "v"))) "holds"   (Bool  "("  (Bool (Bool  "not" (Set (Var "c")) "is"   ($#v1_xboole_0 :::"empty"::: )  )) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "c")))  ($#r1_tarski :::"c="::: )  (Set (Var "X"))) & (Bool (Set (Var "v"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "G"))  ($#k1_graph_3 :::"-VSet"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "c")) ")" )))  ")" ))))) ; 
 
theorem :: GRAPH_3:56 (Bool  "for" (Set (Var "G")) "being"   ($#v5_graph_1 :::"connected"::: )     ($#v6_graph_1 :::"finite"::: )    ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "c")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set (Set (Var "G"))  ($#k9_graph_3 :::"-CycleSet"::: )  )  "st" (Bool (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "c")))  ($#r1_hidden :::"<>"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G")))) & (Bool (Bool  "not" (Set (Var "c")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "holds"  (Bool  "{"  (Set (Var "v9")) where v9 "is"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) : (Bool  "("  (Bool (Set (Var "v9"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "G"))  ($#k1_graph_3 :::"-VSet"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "c")) ")" ))) & (Bool (Set   ($#k10_graph_1 :::"Degree"::: )  (Set (Var "v9")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k7_graph_3 :::"Degree"::: )   "(" (Set (Var "v9")) "," (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "c")) ")" ) ")" ))  ")" )  "}"   "is"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))))) ; 
 definitionlet "G" be   ($#v5_graph_1 :::"connected"::: )     ($#v6_graph_1 :::"finite"::: )    ($#l1_graph_1 :::"Graph":::); let "c" be    ($#m2_finseq_2 :::"Element"::: )   "of" (Set (Set (Const "G"))  ($#k9_graph_3 :::"-CycleSet"::: )  ); assume that  
(Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Const "c")))  ($#r1_hidden :::"<>"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Const "G"))))
 and  
(Bool (Bool  "not" (Set (Const "c")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))
 ; func  :::"ExtendCycle"::: "c" ->    ($#m2_finseq_2 :::"Element"::: )   "of" (Set "G"  ($#k9_graph_3 :::"-CycleSet"::: )  ) means :: GRAPH_3:def 13 (Bool  "ex" (Set (Var "c9")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set "G"  ($#k9_graph_3 :::"-CycleSet"::: )  )(Bool  "ex" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" "G" "st"  (Bool  "("  (Bool (Set (Var "v"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_subset_1 :::"choose"::: )   "{"  (Set (Var "v9")) where v9 "is"   ($#m1_subset_1 :::"Vertex":::) "of" "G" : (Bool  "("  (Bool (Set (Var "v9"))  ($#r2_hidden :::"in"::: )  (Set "G"  ($#k1_graph_3 :::"-VSet"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  "c" ")" ))) & (Bool (Set   ($#k10_graph_1 :::"Degree"::: )  (Set (Var "v9")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k7_graph_3 :::"Degree"::: )   "(" (Set (Var "v9")) "," (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  "c" ")" ) ")" ))  ")" )  "}"  )) & (Bool (Set (Var "c9"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_subset_1 :::"choose"::: )  (Set  "(" (Set  "(" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "G")  ($#k6_subset_1 :::"\"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  "c" ")" ) ")" )  ($#k13_graph_3 :::"-CycleSet"::: )  (Set (Var "v")) ")" ))) & (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k11_graph_3 :::"CatCycles"::: )   "(" "c" "," (Set (Var "c9")) ")" ))  ")" ))); end; 







:: deftheorem    defines :::"ExtendCycle"::: GRAPH_3:def 13 :  (Bool  "for" (Set (Var "G")) "being"   ($#v5_graph_1 :::"connected"::: )     ($#v6_graph_1 :::"finite"::: )    ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "c")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set (Set (Var "G"))  ($#k9_graph_3 :::"-CycleSet"::: )  )  "st" (Bool (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "c")))  ($#r1_hidden :::"<>"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G")))) & (Bool (Bool  "not" (Set (Var "c")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "holds"  (Bool  "for" (Set (Var "b3")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set (Set (Var "G"))  ($#k9_graph_3 :::"-CycleSet"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k14_graph_3 :::"ExtendCycle"::: )  (Set (Var "c")))) "iff" (Bool  "ex" (Set (Var "c9")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set (Set (Var "G"))  ($#k9_graph_3 :::"-CycleSet"::: )  )(Bool  "ex" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st"  (Bool  "("  (Bool (Set (Var "v"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_subset_1 :::"choose"::: )   "{"  (Set (Var "v9")) where v9 "is"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) : (Bool  "("  (Bool (Set (Var "v9"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "G"))  ($#k1_graph_3 :::"-VSet"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "c")) ")" ))) & (Bool (Set   ($#k10_graph_1 :::"Degree"::: )  (Set (Var "v9")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k7_graph_3 :::"Degree"::: )   "(" (Set (Var "v9")) "," (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "c")) ")" ) ")" ))  ")" )  "}"  )) & (Bool (Set (Var "c9"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_subset_1 :::"choose"::: )  (Set  "(" (Set  "(" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G")))  ($#k6_subset_1 :::"\"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "c")) ")" ) ")" )  ($#k13_graph_3 :::"-CycleSet"::: )  (Set (Var "v")) ")" ))) & (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k11_graph_3 :::"CatCycles"::: )   "(" (Set (Var "c")) "," (Set (Var "c9")) ")" ))  ")" )))  ")" )))); 
 
theorem :: GRAPH_3:57 (Bool  "for" (Set (Var "G")) "being"   ($#v5_graph_1 :::"connected"::: )     ($#v6_graph_1 :::"finite"::: )    ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "c")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set (Set (Var "G"))  ($#k9_graph_3 :::"-CycleSet"::: )  )  "st" (Bool (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "c")))  ($#r1_hidden :::"<>"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G")))) & (Bool (Bool  "not" (Set (Var "c")) "is"   ($#v1_xboole_0 :::"empty"::: )  )) & (Bool  "("   "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds"  (Bool (Set   ($#k10_graph_1 :::"Degree"::: )  (Set (Var "v"))) "is"   ($#v1_abian :::"even"::: )  )  ")" )) "holds"  (Bool  "("  (Bool (Bool  "not" (Set   ($#k14_graph_3 :::"ExtendCycle"::: )  (Set (Var "c"))) "is"   ($#v1_xboole_0 :::"empty"::: )  )) & (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "c")) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k14_graph_3 :::"ExtendCycle"::: )  (Set (Var "c")) ")" ) ")" )))  ")" ))) ; 
 begin  definitionlet "G" be   ($#l1_graph_1 :::"Graph":::); let "p" be   ($#m2_graph_1 :::"Path":::) "of" (Set (Const "G")); attr "p" is  :::"Eulerian":::  means :: GRAPH_3:def 14 (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  "p")  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "G")); end; 





:: deftheorem    defines :::"Eulerian"::: GRAPH_3:def 14 :  (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m2_graph_1 :::"Path":::) "of" (Set (Var "G")) "holds"   (Bool  "("  (Bool (Set (Var "p")) "is"   ($#v1_graph_3 :::"Eulerian"::: )  ) "iff" (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G"))))  ")" ))); 
 
theorem :: GRAPH_3:58 (Bool  "for" (Set (Var "G")) "being"   ($#v5_graph_1 :::"connected"::: )    ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m2_graph_1 :::"Path":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "vs")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))  "st" (Bool (Bool (Set (Var "p")) "is"   ($#v1_graph_3 :::"Eulerian"::: )  ) & (Bool (Set (Var "vs"))  ($#r1_graph_2 :::"is_vertex_seq_of"::: )  (Set (Var "p")))) "holds"  (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "vs")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G"))))))) ; 
 
theorem :: GRAPH_3:59 (Bool  "for" (Set (Var "G")) "being"   ($#v5_graph_1 :::"connected"::: )     ($#v6_graph_1 :::"finite"::: )    ($#l1_graph_1 :::"Graph":::) "holds"   (Bool  "("  (Bool  "ex" (Set (Var "p")) "being"   ($#v1_msscyc_1 :::"cyclic"::: )    ($#m2_graph_1 :::"Path":::) "of" (Set (Var "G")) "st" (Bool (Set (Var "p")) "is"   ($#v1_graph_3 :::"Eulerian"::: )  )) "iff" (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds"  (Bool (Set   ($#k10_graph_1 :::"Degree"::: )  (Set (Var "v"))) "is"   ($#v1_abian :::"even"::: )  ))  ")" )) ; 
 
theorem :: GRAPH_3:60 (Bool  "for" (Set (Var "G")) "being"   ($#v5_graph_1 :::"connected"::: )     ($#v6_graph_1 :::"finite"::: )    ($#l1_graph_1 :::"Graph":::) "holds"   (Bool  "("  (Bool  "ex" (Set (Var "p")) "being"   ($#m2_graph_1 :::"Path":::) "of" (Set (Var "G")) "st"  (Bool  "("  (Bool (Bool  "not" (Set (Var "p")) "is"   ($#v1_msscyc_1 :::"cyclic"::: )  )) & (Bool (Set (Var "p")) "is"   ($#v1_graph_3 :::"Eulerian"::: )  )  ")" )) "iff" (Bool  "ex" (Set (Var "v1")) "," (Set (Var "v2")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st"  (Bool  "("  (Bool (Set (Var "v1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "v2"))) & (Bool  "("   "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds"   (Bool  "("  (Bool (Set   ($#k10_graph_1 :::"Degree"::: )  (Set (Var "v"))) "is"   ($#v1_abian :::"even"::: )  ) "iff" (Bool  "("  (Bool (Set (Var "v"))  ($#r1_hidden :::"<>"::: )  (Set (Var "v1"))) & (Bool (Set (Var "v"))  ($#r1_hidden :::"<>"::: )  (Set (Var "v2")))  ")" )  ")" )  ")" )  ")" ))  ")" )) ;