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 )
set X = DTrSpace (V,w,y);
assume A1: Gen w,y ; :: thesis: DTrSpace (V,w,y) is MidOrdTrapSpace
DTrSpace (V,w,y) is MidOrdTrapSpace-like by Lm27, Lm28, Lm29, Lm30, Lm31, A1, Lm32, Lm33, Lm34, Lm35, Lm22, Lm23, Lm24, Lm25, Lm26;
hence DTrSpace (V,w,y) is MidOrdTrapSpace ; :: thesis: verum