take F_Complex ; :: thesis: ( F_Complex is quadratic_complete & F_Complex is strict )
thus ( F_Complex is quadratic_complete & F_Complex is strict ) ; :: thesis: verum