consider F being Field;
take F ; :: thesis: ( F is add-associative & F is right_complementable & F is right_zeroed )
thus ( F is add-associative & F is right_complementable & F is right_zeroed ) ; :: thesis: verum