AMSpace V0,w0,y0 is OrtAfSp-like by Def9, Lm8;
hence ex b₁ being non empty ParOrtStr st
( b₁ is strict & b₁ is OrtAfSp-like ) ; :: thesis: verum