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