TernaryFieldEx is Ternary-Field-like by Def7, Lm1, Lm2, Lm3, Lm4, Lm5, Lm6, Lm7, Lm8, Lm9;
hence ex b₁ being non empty TernaryFieldStr st
( b₁ is strict & b₁ is Ternary-Field-like ) ; :: thesis: verum