set
G
= the
Group
;
take
(1).
the
Group
;
:: thesis:
(
(1).
the
Group
is
strict
&
(1).
the
Group
is
finite
)
thus
(
(1).
the
Group
is
strict
&
(1).
the
Group
is
finite
) ;
:: thesis:
verum