take F_Real ; :: thesis: ( F_Real is gcd-like & F_Real is associative & F_Real is commutative & F_Real is well-unital & F_Real is domRing-like & F_Real is unital & F_Real is distributive & not F_Real is degenerated & F_Real is Abelian & F_Real is add-associative & F_Real is right_zeroed & F_Real is right_complementable )
thus ( F_Real is gcd-like & F_Real is associative & F_Real is commutative & F_Real is well-unital & F_Real is domRing-like & F_Real is unital & F_Real is distributive & not F_Real is degenerated & F_Real is Abelian & F_Real is add-associative & F_Real is right_zeroed & F_Real is right_complementable ) ; :: thesis: verum