take F_Rat ; :: thesis: ( not F_Rat is 2 -characteristic & F_Rat is strict )
Char F_Rat = 0 by RING_3:def 6;
hence ( not F_Rat is 2 -characteristic & F_Rat is strict ) ; :: thesis: verum