set M1 = (M0 +* ((*' {t}) --> FALSE)) +* (({t} *') --> TRUE);
M0 +* ((*' {t}) --> FALSE) is Function of the carrier of PTN,BOOLEAN by Th1;
then (M0 +* ((*' {t}) --> FALSE)) +* (({t} *') --> TRUE) is Function of the carrier of PTN,BOOLEAN by Th1;
hence (M0 +* ((*' {t}) --> FALSE)) +* (({t} *') --> TRUE) is Boolean_marking of PTN by FUNCT_2:8; :: thesis: verum