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