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