set F = the Field;
take the Field ; :: thesis: not the Field is trivial
thus not the Field is trivial ; :: thesis: verum