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