:: deftheorem Def11 defines MidOrdTrapSpace-like GEOMTRAP:def 12 :
for IT being non empty AfMidStruct holds
( IT is MidOrdTrapSpace-like iff for a, b, c, d, a1, b1, c1, d1, p, q being Element of IT holds
( a # b = b # a & a # a = a & (a # b) # (c # d) = (a # c) # (b # d) & ex p being Element of IT st p # a = b & ( a # b = a # c implies b = c ) & ( a,b // c,d implies a,b // a # c,b # d ) & ( not a,b // c,d or a,b // a # d,b # c or a,b // b # c,a # d ) & ( a,b // c,d & a # a1 = p & b # b1 = p & c # c1 = p & d # d1 = p implies a1,b1 // c1,d1 ) & ( p <> q & p,q // a,a1 & p,q // b,b1 & p,q // c,c1 & p,q // d,d1 & a,b // c,d implies a1,b1 // c1,d1 ) & ( 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 ) ) );