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