let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V st Gen w,y holds
DTrSpace V,w,y is MidOrdTrapSpace
let w, y be VECTOR of V; :: thesis: ( Gen w,y implies DTrSpace V,w,y is MidOrdTrapSpace )
assume A1: Gen w,y ; :: thesis: DTrSpace V,w,y is MidOrdTrapSpace
set X = DTrSpace V,w,y;
for a, b, c, d, a1, b1, c1, d1, p, q being Element of (DTrSpace V,w,y) holds
( a # b = b # a & a # a = a & (a # b) # (c # d) = (a # c) # (b # d) & ex p being Element of (DTrSpace V,w,y) 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 (DTrSpace V,w,y) st
( a,b // c,d or a,b // d,c ) & ( a,b // c,p & a,b // c,q & not a = b implies p = q ) ) by A1, Lm21, Lm22, Lm23, Lm24, Lm25, Lm26, Lm27, Lm28, Lm29, Lm30, Lm31, Lm32, Lm33, Lm34;
hence DTrSpace V,w,y is MidOrdTrapSpace by Def13; :: thesis: verum