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