defpred S₁[ set ] means [$1,x] in the Flow of N;
thus ex IT being set st
for y being set holds
( y in IT iff ( y in the Places of N & S₁[y] ) ) from XBOOLE_0:sch 1(); :: thesis: verum