set u = the Element of UN;
take [ the Element of UN, the Element of UN] ; :: thesis: [ the Element of UN, the Element of UN] is pair
thus [ the Element of UN, the Element of UN] is pair ; :: thesis: verum