take
F_Real
; :: thesis: ( F_Real is strict & F_Real is Abelian & F_Real is add-associative & F_Real is commutative & F_Real is associative & F_Real is distributive & not F_Real is degenerated & F_Real is left_zeroed & F_Real is right_zeroed & F_Real is Loop-like & F_Real is well-unital & F_Real is multLoop_0-like )

thus ( F_Real is strict & F_Real is Abelian & F_Real is add-associative & F_Real is commutative & F_Real is associative & F_Real is distributive & not F_Real is degenerated & F_Real is left_zeroed & F_Real is right_zeroed & F_Real is Loop-like & F_Real is well-unital & F_Real is multLoop_0-like ) ; :: thesis: verum

thus ( F_Real is strict & F_Real is Abelian & F_Real is add-associative & F_Real is commutative & F_Real is associative & F_Real is distributive & not F_Real is degenerated & F_Real is left_zeroed & F_Real is right_zeroed & F_Real is Loop-like & F_Real is well-unital & F_Real is multLoop_0-like ) ; :: thesis: verum