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