let x be Element of P; :: thesis: x is pair
consider y, z being object such that
A1: x = [y,z] by RELAT_1:def 1;
thus x is pair by A1; :: thesis: verum