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

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