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