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