ex m1, m2 being marking of P st t = [m1,m2] by Def6;
hence Post is marking of P by MCART_1:7; :: thesis: verum