defpred S₁[ finite _Graph] means ( $1 is connected implies $1 .order() <= ($1 .size() ) + 1 );
A1: for G being finite _Graph st G .order() = 1 holds
S₁[G] by NAT_1:12;

A2: 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 A3: 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 A4: Gk1 .order() = k + 1 ; :: thesis: S₁[Gk1]

now

assume A5: Gk1 is connected ; :: thesis: Gk1 .order() <= (Gk1 .size() ) + 1

now

assume Gk1 .order() = 1 ; :: thesis: contradiction
then k + 1 = 0 + 1 by A4;
hence contradiction ; :: thesis: verum

end;

then reconsider Gk1' = Gk1 as finite non trivial connected _Graph by A5, GLIB_000:29;
consider v1, v2 being Vertex of Gk1' such that
A6: ( v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex ) by Lm21;
consider Gkb being removeVertex of Gk1',v1;
A7: Gkb is connected by A6, Lm20;
( (Gkb .order() ) + 1 = k + 1 & (Gkb .size() ) + (card (v1 .edgesInOut() )) = Gk1 .size() ) by A4, GLIB_000:51;
then A8: k <= ((Gk1 .size() ) - (card (v1 .edgesInOut() ))) + 1 by A3, A7;
not v1 is isolated by Th2;
then v1 .edgesInOut() <> {} by GLIB_000:def 51;
then card (v1 .edgesInOut() ) <> 0 ;
then 0 < card (v1 .edgesInOut() ) by NAT_1:3;
then 0 + 1 <= card (v1 .edgesInOut() ) by NAT_1:13;
then k + 1 <= (((Gk1 .size() ) + 1) - (card (v1 .edgesInOut() ))) + (card (v1 .edgesInOut() )) by A8, XREAL_1:9;
hence Gk1 .order() <= (Gk1 .size() ) + 1 by A4; :: thesis: verum

end;

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

end;

A9: for G being finite _Graph holds S₁[G] from GLIB_000:sch 1(A1, A2);
let G be finite connected _Graph; :: thesis: G .order() <= (G .size() ) + 1
thus G .order() <= (G .size() ) + 1 by A9; :: thesis: verum