consider x being non pair set ;
take {x} ; :: thesis: not {x} is with_pair
thus not {x} is with_pair ; :: thesis: verum