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