let G2 be SimpleGraph 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 Th136;
hence G2 is connected by Th36; :: thesis: verum