set F = the Field;
take the Field ; :: thesis: ( the Field is add-associative & the Field is right_complementable & the Field is right_zeroed )
thus ( the Field is add-associative & the Field is right_complementable & the Field is right_zeroed ) ; :: thesis: verum