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