@MISC{GLENUM00.MIZ,
  AUTHOR = {Koch, Sebastian},
  TITLE = {Introduction to Graph Enumerations},
  SECTION1 = {Subgraph set and Subgraph Relation},
  SECTION2 = {Induced Subgraph set},
  SECTION3 = {Spanning Subgraph set},
  SECTION4 = {Forest Subgraph set},
  SECTION5 = {Spanning Forest Subgraph set},
  SECTION6 = {Connected Subgraph set},
  SECTION7 = {Tree Subgraph set and Subtree Relation},
  SECTION8 = {Spanning Tree Subgraph set},
  SECTION9 = {Component Subgraph set},
  DAY = {31},
  MONTH = {March},
  YEAR = {2023},
  ADDRESS1 = {Germany\\\href{mailto:fly.high.android@gmail.com}{fly.high.android@gmail.com}},
  SUMMARY = {In this article sets of certain subgraphs of a graph are formalized in 
   the Mizar system\cite{FourDecades}, based on the formalization of graphs in 
   \cite{GLIB_000.ABS}. The main result is the spanning subgraph theorem.},
  INTRODUCTION = {Subsets of the set of all subgraphs of a graphs are rather rarely 
    addressed directly, but used as a tool in a wide variety of graph theory topics;
  e.g. they are needed for graph factorisation, graph reconstruction, random graphs, 
  counting a special type of subgraphs and proving that every connected graph has a 
  spanning subgraph (cf. \cite{MULTI}, \cite{SIMPLE}, cite{DIESTEL}).
  The latter is proven in Section 7 of this article, together with the sharper result 
  that we can even guarantee a spanning graph containing an arbitrary edge of the connected graph.
  As a necessity for that the set of all subtrees of a graph was introduced, as Jessica Enright 
  and Piotr Rudnicki wished for in \cite{HELLY.ABS}.
  This article lays the groundwork for further formalization of any of these topics. 
  It is noteworthy that the attribute \texttt{plain} from \cite{GLIB_009.ABS} was utilized here.}}
  
@Article{BancerekJAR:2018,
  author={Bancerek, Grzegorz and Byli{\'{n}}ski, Czes{\l}aw and Grabowski, Adam and Korni{\l}owicz, Artur and Matuszewski, Roman and Naumowicz, Adam and P{\k{a}}k, Karol},
  title={The Role of the {M}izar {M}athematical {L}ibrary for Interactive Proof Development in {M}izar},
  journal={Journal of Automated Reasoning},
  year={2018},
  volume={61},
  number={1},
  pages={9--32},
  doi={10.1007/s10817-017-9440-6},
  url={https://doi.org/10.1007/s10817-017-9440-6}
}

@Article{FourDecades,
  author={Grabowski, Adam and Korni{\l}owicz, Artur and Naumowicz, Adam},
  title={Four Decades of {M}izar},
  journal={Journal of Automated Reasoning},
  year={2015},
  volume={55},
  number={3},
  pages={191--198},
  issn={1573-0670},
  doi={10.1007/s10817-015-9345-1}
}

@book{SIMPLE,
  TITLE = {Introduction to graph theory},
  AUTHOR = {Wilson, Robin James},
  ADDRESS = {Edinburgh},
  PUBLISHER = {Oliver & Boyd},
  YEAR = {1972},
  ISBN = {0-05-002534-1},
  PAGES = {VIII, 168 p.},
  URL = {http://scans.hebis.de/HEBCGI/show.pl?10670775_toc.pdf},

}
@book{DIESTEL,
  TITLE = {Graph theory},
  VOLUME = {Graduate texts in mathematics ; 173},
  AUTHOR = {Diestel, Reinhard [Verfasser]},
  ADDRESS = {Berlin},
  PUBLISHER = {Springer},
  YEAR = {[2017]},
  EDITION = {Fifth edition},
  ISBN = {978-3-662-53621-6},
  PAGES = {XVIII, 428 p.}
}

@book{MULTI,
  TITLE = {Graph theory},
  SERIES = {Graduate texts in mathematics ; 244},
  AUTHOR = {Bondy, John Adrian ; Murty, U. S. R.},
  ADDRESS = {New York, NY},
  PUBLISHER = {Springer},
  YEAR = {2008},
  ISBN = {978-1-84628-969-9},
  PAGES = {XII, 652 p.},
  URL = {http://scans.hebis.de/HEBCGI/show.pl?19542627_toc.pdf ; http://scans.hebis.de/HEBCGI/show.pl?19542627_kap-2.pdf ; http://scans.hebis.de/HEBCGI/show.pl?19542627_ein-1.pdf}
}