G .order() is finite by Th6;
hence ( not G .order() is zero & G .order() is natural ) ; :: thesis: verum