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