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 distributive & F_Real is almost_left_invertible & F_Real is well-unital & not F_Real is trivial )
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 distributive & F_Real is almost_left_invertible & F_Real is well-unital & not F_Real is trivial ) ; :: thesis: verum