:: deftheorem defines TrapSpace-like GEOMTRAP:def 14 :
for IT being non empty AffinStruct holds
( IT is TrapSpace-like iff for a9, b9, c9, d9, p9, q9 being Element of IT holds
( a9,b9 // b9,a9 & ( a9,b9 // c9,d9 & a9,b9 // c9,q9 & not a9 = b9 implies d9 = q9 ) & ( p9 <> q9 & p9,q9 // a9,b9 & p9,q9 // c9,d9 implies a9,b9 // c9,d9 ) & ( a9,b9 // c9,d9 implies c9,d9 // a9,b9 ) & ex x9 being Element of IT st a9,b9 // c9,x9 ) );