let PTN be Petri_net; :: thesis: for t being transition of PTN
for S0 being Subset of the carrier of PTN holds
( t in S0 *' iff *' {t} meets S0 )
let t be transition of PTN; :: thesis: for S0 being Subset of the carrier of PTN holds
( t in S0 *' iff *' {t} meets S0 )
let S0 be Subset of the carrier of PTN; :: thesis: ( t in S0 *' iff *' {t} meets S0 )
thus ( t in S0 *' implies *' {t} meets S0 ) :: thesis: ( *' {t} meets S0 implies t in S0 *' )

proof

assume t in S0 *' ; :: thesis: *' {t} meets S0
then consider f being S-T_arc of PTN, s being place of PTN such that
A1: s in S0 and
A2: f = [s,t] by Th4;
t in {t} by TARSKI:def 1;
then s in *' {t} by A2;
hence (*' {t}) /\ S0 <> {} by A1, XBOOLE_0:def 4; :: according to XBOOLE_0:def 7 :: thesis: verum

end;

assume (*' {t}) /\ S0 <> {} ; :: according to XBOOLE_0:def 7 :: thesis: t in S0 *'
then consider s being place of PTN such that
A3: s in (*' {t}) /\ S0 by SUBSET_1:4;
A4: s in S0 by A3, XBOOLE_0:def 4;
s in *' {t} by A3, XBOOLE_0:def 4;
then consider f being S-T_arc of PTN, t0 being transition of PTN such that
A5: t0 in {t} and
A6: f = [s,t0] by Th6;
t0 = t by A5, TARSKI:def 1;
hence t in S0 *' by A4, A6; :: thesis: verum