take F_Real ; :: thesis: ( not F_Real is quadratic_complete & F_Real is polynomial_disjoint & F_Real is strict )
thus ( not F_Real is quadratic_complete & F_Real is polynomial_disjoint & F_Real is strict ) ; :: thesis: verum