take F_Real ; :: thesis: ( F_Real is commutative & F_Real is associative & F_Real is unital )
thus ( F_Real is commutative & F_Real is associative & F_Real is unital ) ; :: thesis: verum