take F_Real ; :: thesis: ( F_Real is preordered & F_Real is polynomial_disjoint )
thus ( F_Real is preordered & F_Real is polynomial_disjoint ) ; :: thesis: verum