theorem Th25: :: WAYBEL11:25

for S being non empty 1-sorted
for e being Element of S
for x being Element of (Net-Str e) holds x = e