set x = the non pair set ;
take { the non pair set } ; :: thesis: not { the non pair set } is with_pair
thus not { the non pair set } is with_pair ; :: thesis: verum