let G2 be removeLoops of G; :: thesis: G2 is connected
for W1 being Walk of G ex W2 being Walk of G2 st W2 is_Walk_from W1 .first() ,W1 .last() by Th61;
hence G2 is connected by Th36; :: thesis: verum