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