let G1 be addAdjVertexAll of G,v, {} ; :: thesis: not G1 is connected
G1 is addVertex of G,v by Th55;
hence not G1 is connected ; :: thesis: verum