let G be finite connected _Graph; :: thesis: G .order() <= (G .size()) + 1

defpred S_{1}[ finite _Graph] means ( $1 is connected implies $1 .order() <= ($1 .size()) + 1 );

S_{1}[G]
by NAT_1:12;

for G being finite _Graph holds S_{1}[G]
from GLIB_000:sch 1(A8, A1);

hence G .order() <= (G .size()) + 1 ; :: thesis: verum

defpred S

A1: now :: thesis: for k being non zero Nat st ( for Gk being finite _Graph st Gk .order() = k holds

S_{1}[Gk] ) holds

for Gk1 being finite _Graph st Gk1 .order() = k + 1 holds

S_{1}[Gk1]

A8:
for G being finite _Graph st G .order() = 1 holds S

for Gk1 being finite _Graph st Gk1 .order() = k + 1 holds

S

let k be non zero Nat; :: thesis: ( ( for Gk being finite _Graph st Gk .order() = k holds

S_{1}[Gk] ) implies for Gk1 being finite _Graph st Gk1 .order() = k + 1 holds

S_{1}[Gk1] )

assume A2: for Gk being finite _Graph st Gk .order() = k holds

S_{1}[Gk]
; :: thesis: for Gk1 being finite _Graph st Gk1 .order() = k + 1 holds

S_{1}[Gk1]

let Gk1 be finite _Graph; :: thesis: ( Gk1 .order() = k + 1 implies S_{1}[Gk1] )

assume A3: Gk1 .order() = k + 1 ; :: thesis: S_{1}[Gk1]

_{1}[Gk1]
; :: thesis: verum

end;S

S

assume A2: for Gk being finite _Graph st Gk .order() = k holds

S

S

let Gk1 be finite _Graph; :: thesis: ( Gk1 .order() = k + 1 implies S

assume A3: Gk1 .order() = k + 1 ; :: thesis: S

now :: thesis: ( Gk1 is connected implies 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 Th1;

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
SA4: now :: thesis: not Gk1 .order() = 1

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

then k + 1 = 0 + 1 by A3;

hence contradiction ; :: thesis: verum

end;then k + 1 = 0 + 1 by A3;

hence contradiction ; :: thesis: verum

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 Th1;

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

S

for G being finite _Graph holds S

hence G .order() <= (G .size()) + 1 ; :: thesis: verum