consider n being non zero Nat such that
A: order F = (Char F) |^ n by FIELD_15:92;
thus not order F is trivial by A; :: thesis: verum