take the Field ; :: thesis: the Field is PID
thus the Field is PID ; :: thesis: verum