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

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