consider V being RealLinearSpace such that
A1: ex w, y being VECTOR of V st Gen w,y by ANALMETR:3;
consider w, y being VECTOR of V such that
A2: Gen w,y by A1;
set X = DTrSpace (V,w,y);
DTrSpace (V,w,y) is MidOrdTrapSpace-like

let a, b, c, d, a1, b1, c1, d1, p, q be Element of (DTrSpace (V,w,y)); :: according to GEOMTRAP:def 12 :: thesis:
thus ( a # b = b # a & a # a = a & (a # b) # (c # d) = (a # c) # (b # d) ) by Lm27, Lm28, Lm29; :: thesis:
thus ex p being Element of (DTrSpace (V,w,y)) st p # a = b by Lm30; :: thesis:
thus ( a # b = a # c implies b = c ) by Lm31; :: thesis:
thus ( a,b // c,d implies a,b // a # c,b # d ) by A2, Lm32; :: thesis:
thus ( not a,b // c,d or a,b // a # d,b # c or a,b // b # c,a # d ) by A2, Lm33; :: thesis:
thus ( a,b // c,d & a # a1 = p & b # b1 = p & c # c1 = p & d # d1 = p implies a1,b1 // c1,d1 ) by Lm34; :: thesis:
thus ( 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 ) by A2, Lm35; :: thesis:
thus ( a,b // b,c implies ( a = b & b = c ) ) by A2, Lm22; :: thesis:
thus ( a,b // a1,b1 & a,b // c1,d1 & a <> b implies a1,b1 // c1,d1 ) by A2, Lm23; :: thesis:
thus ( a,b // c,d implies ( c,d // a,b & b,a // d,c ) ) by Lm24; :: thesis:
thus ex d being Element of (DTrSpace (V,w,y)) st
( a,b // c,d or a,b // d,c ) by A2, Lm25; :: thesis:
thus ( a,b // c,p & a,b // c,q & not a = b implies p = q ) by A2, Lm26; :: thesis:

end;