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