let G be non edgeless _Graph; :: thesis: for e being Edge of G st not e in G .loops() holds
createGraph e in G .allTrees()
let e be Edge of G; :: thesis: ( not e in G .loops() implies createGraph e in G .allTrees() )
assume not e in G .loops() ; :: thesis: createGraph e in G .allTrees()
then ( createGraph e is connected & createGraph e is acyclic ) by Th18;
hence createGraph e in G .allTrees() by Th138; :: thesis: verum