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