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