set TS = Lambda the OrdTrapSpace;
Lambda the OrdTrapSpace is TrapSpace-like by Lm43;
hence ex b₁ being non empty AffinStruct st
( b₁ is strict & b₁ is TrapSpace-like ) ; :: thesis: verum