consider F being non degenerated strict Field;
take F ; :: thesis: ( F is strict & F is Abelian & F is add-associative & F is right_zeroed & F is right_complementable & F is associative & F is commutative & F is distributive & F is unital & F is domRing-like & F is almost_left_invertible & not F is degenerated & not F is trivial )
thus ( F is strict & F is Abelian & F is add-associative & F is right_zeroed & F is right_complementable & F is associative & F is commutative & F is distributive & F is unital & F is domRing-like & F is almost_left_invertible & not F is degenerated & not F is trivial ) ; :: thesis: verum