let G be finite connected _Graph; :: thesis: G .order() <= () + 1
defpred S1[ finite _Graph] means ( \$1 is connected implies \$1 .order() <= (\$1 .size()) + 1 );
A1: now :: thesis: for k being non zero Nat st ( for Gk being finite _Graph st Gk .order() = k holds
S1[Gk] ) holds
for Gk1 being finite _Graph st Gk1 .order() = k + 1 holds
S1[Gk1]
let k be non zero Nat; :: thesis: ( ( for Gk being finite _Graph st Gk .order() = k holds
S1[Gk] ) implies for Gk1 being finite _Graph st Gk1 .order() = k + 1 holds
S1[Gk1] )

assume A2: for Gk being finite _Graph st Gk .order() = k holds
S1[Gk] ; :: thesis: for Gk1 being finite _Graph st Gk1 .order() = k + 1 holds
S1[Gk1]

let Gk1 be finite _Graph; :: thesis: ( Gk1 .order() = k + 1 implies S1[Gk1] )
assume A3: Gk1 .order() = k + 1 ; :: thesis: S1[Gk1]
now :: thesis: ( Gk1 is connected implies Gk1 .order() <= (Gk1 .size()) + 1 )
A4: now :: thesis: not Gk1 .order() = 1
assume Gk1 .order() = 1 ; :: thesis: contradiction
then k + 1 = 0 + 1 by A3;
hence contradiction ; :: thesis: verum
end;
assume Gk1 is connected ; :: thesis: Gk1 .order() <= (Gk1 .size()) + 1
then reconsider Gk19 = Gk1 as finite non trivial connected _Graph by ;
consider v1, v2 being Vertex of Gk19 such that
v1 <> v2 and
A5: not v1 is cut-vertex and
not v2 is cut-vertex by Lm21;
set Gkb = the removeVertex of Gk19,v1;
A6: ( ( the removeVertex of Gk19,v1 .order()) + 1 = k + 1 & ( the removeVertex of Gk19,v1 .size()) + (card ()) = Gk1 .size() ) by ;
not v1 is isolated by Th1;
then v1 .edgesInOut() <> {} by GLIB_000:def 49;
then 0 < card () by NAT_1:3;
then A7: 0 + 1 <= card () by NAT_1:13;
the removeVertex of Gk19,v1 is connected by ;
then k <= ((Gk1 .size()) - (card ())) + 1 by A2, A6;
then k + 1 <= (((Gk1 .size()) + 1) - (card ())) + (card ()) by ;
hence Gk1 .order() <= (Gk1 .size()) + 1 by A3; :: thesis: verum
end;
hence S1[Gk1] ; :: thesis: verum
end;
A8: for G being finite _Graph st G .order() = 1 holds
S1[G] by NAT_1:12;
for G being finite _Graph holds S1[G] from hence G .order() <= () + 1 ; :: thesis: verum