:: deftheorem Def12 defines OrdTrapSpace-like GEOMTRAP:def 13 :
for IT being non empty AffinStruct holds
( IT is OrdTrapSpace-like iff for a, b, c, d, a1, b1, c1, d1, p, q being Element of IT holds
( ( a,b // b,c implies ( a = b & b = c ) ) & ( a,b // a1,b1 & a,b // c1,d1 & a <> b implies a1,b1 // c1,d1 ) & ( a,b // c,d implies ( c,d // a,b & b,a // d,c ) ) & ex d being Element of IT st
( a,b // c,d or a,b // d,c ) & ( a,b // c,p & a,b // c,q & not a = b implies p = q ) ) );