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