take
the non
empty
finite
Subset
of
T
;
:: thesis:
( the non
empty
finite
Subset
of
T
is
finite
& not the non
empty
finite
Subset
of
T
is
empty
)
thus
( the non
empty
finite
Subset
of
T
is
finite
& not the non
empty
finite
Subset
of
T
is
empty
) ;
:: thesis:
verum