take F_Rat ; :: thesis: ( F_Rat is strict & F_Rat is polynomial_disjoint & not F_Rat is quadratic_complete & not F_Rat is 2 -characteristic )
Char F_Rat <> 2 by RING_3:def 6;
hence ( F_Rat is strict & F_Rat is polynomial_disjoint & not F_Rat is quadratic_complete & not F_Rat is 2 -characteristic ) by RING_3:def 6; :: thesis: verum