defpred S₁[ set ] means ex f being S-T_arc of PTN ex t being transition of PTN st
( t in T0 & f = [$1,t] );
{ s where s is place of PTN : S₁[s] } is Subset of the carrier of PTN from DOMAIN_1:sch 7();
hence { s where s is place of PTN : ex f being S-T_arc of PTN ex t being transition of PTN st
( t in T0 & f = [s,t] ) } is Subset of the carrier of PTN ; :: thesis: verum