consider OTS being OrdTrapSpace;
set TS = Lambda OTS;
for a', b', c', d', p', q' being Element of (Lambda OTS) holds
( a',b' // b',a' & ( a',b' // c',d' & a',b' // c',q' & not a' = b' implies d' = q' ) & ( p' <> q' & p',q' // a',b' & p',q' // c',d' implies a',b' // c',d' ) & ( a',b' // c',d' implies c',d' // a',b' ) & ex x' being Element of (Lambda OTS) st a',b' // c',x' ) by Lm36, Lm37, Lm38, Lm39, Lm41;
then Lambda OTS is TrapSpace-like by Def15;
hence ex b₁ being non empty AffinStruct st
( b₁ is strict & b₁ is TrapSpace-like ) ; :: thesis: verum