let G be finite connected _Graph; :: thesis: G .order() <= (G .size()) + 1
defpred S₁[ finite _Graph] means ( $1 is connected implies $1 .order() <= ($1 .size()) + 1 );

A1: now

let k be non empty Nat; :: thesis: ( ( for Gk being finite _Graph st Gk .order() = k holds
S₁[Gk] ) implies for Gk1 being finite _Graph st Gk1 .order() = k + 1 holds
S₁[Gk1] )
assume A2: for Gk being finite _Graph st Gk .order() = k holds
S₁[Gk] ; :: thesis: for Gk1 being finite _Graph st Gk1 .order() = k + 1 holds
S₁[Gk1]
let Gk1 be finite _Graph; :: thesis: ( Gk1 .order() = k + 1 implies S₁[Gk1] )
assume A3: Gk1 .order() = k + 1 ; :: thesis: S₁[Gk1]

now

A4: now

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 A4, GLIB_000:26;
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 (v1 .edgesInOut())) = Gk1 .size() ) by A3, GLIB_000:48;
not v1 is isolated by Th2;
then v1 .edgesInOut() <> {} by GLIB_000:def 49;
then 0 < card (v1 .edgesInOut()) by NAT_1:3;
then A7: 0 + 1 <= card (v1 .edgesInOut()) by NAT_1:13;
the removeVertex of Gk19,v1 is connected by A5, Lm20;
then k <= ((Gk1 .size()) - (card (v1 .edgesInOut()))) + 1 by A2, A6;
then k + 1 <= (((Gk1 .size()) + 1) - (card (v1 .edgesInOut()))) + (card (v1 .edgesInOut())) by A7, XREAL_1:7;
hence Gk1 .order() <= (Gk1 .size()) + 1 by A3; :: thesis: verum

end;

hence S₁[Gk1] ; :: thesis: verum

end;

A8: for G being finite _Graph st G .order() = 1 holds
S₁[G] by NAT_1:12;
for G being finite _Graph holds S₁[G] from GLIB_000:sch 1(A8, A1);
hence G .order() <= (G .size()) + 1 ; :: thesis: verum