let G1 be non locally-finite _Graph; :: thesis: for v being Vertex of G1
for G2 being removeVertex of G1,v st v .edgesInOut() is finite holds
not G2 is locally-finite
let v be Vertex of G1; :: thesis: for G2 being removeVertex of G1,v st v .edgesInOut() is finite holds
not G2 is locally-finite
let G2 be removeVertex of G1,v; :: thesis: ( v .edgesInOut() is finite implies not G2 is locally-finite )
assume A1: v .edgesInOut() is finite ; :: thesis: not G2 is locally-finite
for w being Vertex of G1 st w in {v} holds
w .edgesInOut() is finite by A1, TARSKI:def 1;
hence not G2 is locally-finite by Th30; :: thesis: verum