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 by Lm27, Lm28, Lm29, Lm30, Lm31, A2, Lm32, Lm33, Lm34, Lm35, Lm22, Lm23, Lm24, Lm25, Lm26;
hence ex b₁ being non empty AfMidStruct st
( b₁ is strict & b₁ is MidOrdTrapSpace-like ) ; :: thesis: verum