( AffinStruct(# the carrier of the WeakAffVect,P #) is WeakAffSegm-like & not AffinStruct(# the carrier of the WeakAffVect,P #) is trivial ) by Lm16;
hence ex b₁ being non trivial AffinStruct st
( b₁ is strict & b₁ is WeakAffSegm-like ) ; :: thesis: verum