set M = MidStr(# S,(@ w) #);
set W = Atlas w;
Atlas w is associating by A1, Th25;
hence MidStr(# S,(@ w) #) is strict MidSp by A1, Th20; :: thesis: verum