set G = the well-founded Graph;
the well-founded Graph is directed_cycle-less ;
hence ex b₁ being Graph st b₁ is directed_cycle-less ; :: thesis: verum