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