set M = MidStr(# S,(@ w) #);
set W = Atlas w;
MidStr(# S,(@ w) #),G are_associated_wrp Atlas w by A1, Th32;
hence MidStr(# S,(@ w) #) is strict MidSp by A1, Th23; :: thesis: verum