take F_Rat ; :: thesis: F_Rat is strong_polynomial_disjoint
thus F_Rat is strong_polynomial_disjoint ; :: thesis: verum