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 T-S_arc of PTN, s being place of PTN such that
A1: s in S0 and
A2: f = [t,s] by Th2;
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 T-S_arc of PTN, t0 being transition of PTN such that
A5: t0 in {t} and
A6: f = [t0,s] by Th8;
t0 = t by A5, TARSKI:def 1;
hence t in *' S0 by A4, A6; :: thesis: verum