:: deftheorem Def5 defines CongrSpace-like TRANSGEO:def 5 :
for IT being non empty AffinStruct holds
( IT is CongrSpace-like iff ( ( for x, y, z, t, a, b being Element of IT st x,y // a,b & a,b // z,t & a <> b holds
x,y // z,t ) & ( for x, y, z being Element of IT holds x,x // y,z ) & ( for x, y, z, t being Element of IT st x,y // z,t holds
z,t // x,y ) & ( for x, y being Element of IT holds x,y // x,y ) ) );