let
b
be
Nat
;
:: thesis:
(
b
+
1
)
!
>=
2
|^
b
per
cases
(
b
>=
2 or
b
=
0
or
b
=
1 )
by
NAT_1:23
;
suppose
b
>=
2 ;
:: thesis:
(
b
+
1
)
!
>=
2
|^
b
hence
(
b
+
1)
!
>=
2
|^
b
by
Th22
;
:: thesis:
verum
end;
suppose
b
=
0
;
:: thesis:
(
b
+
1
)
!
>=
2
|^
b
hence
(
b
+
1)
!
>=
2
|^
b
by
NEWTON:4
,
NEWTON:13
;
:: thesis:
verum
end;
suppose
b
=
1 ;
:: thesis:
(
b
+
1
)
!
>=
2
|^
b
hence
(
b
+
1)
!
>=
2
|^
b
by
NEWTON:14
;
:: thesis:
verum
end;
end;