reconsider O1 = (order F) + 1 as Nat by TARSKI:1;
(order F) + 1 = (O1 - 1) + 1 ;
hence order F is integer by XXREAL_3:11; :: thesis: verum