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