Af the MidOrdTrapSpace is OrdTrapSpace-like by Def14, Lm36;
hence ex b₁ being non empty AffinStruct st
( b₁ is strict & b₁ is OrdTrapSpace-like ) ; :: thesis: verum