take F_Real ; :: thesis: ( F_Real is add-associative & F_Real is associative & F_Real is right_zeroed & F_Real is left_zeroed & F_Real is well-unital & F_Real is right_complementable & F_Real is distributive )
thus ( F_Real is add-associative & F_Real is associative & F_Real is right_zeroed & F_Real is left_zeroed & F_Real is well-unital & F_Real is right_complementable & F_Real is distributive ) ; :: thesis: verum