set m1 = the marking of P;
take [ the marking of P, the marking of P] ; :: thesis: ex m1, m2 being marking of P st [ the marking of P, the marking of P] = [m1,m2]
thus ex m1, m2 being marking of P st [ the marking of P, the marking of P] = [m1,m2] ; :: thesis: verum