take
Z/
3 ;
:: thesis:
Z/
3 is
finite
thus
Z/
3 is
finite
;
:: thesis:
verum