theorem :: FOMODEL2:28

for S being Language
for s being Element of S
for w being string of S holds
( s is {w} -occurring iff s in rng w ) by FOMODEL0:45;