set I = the Relation of {{}},{{}};
not ContextStr(# {{}},{{}}, the Relation of {{}},{{}} #) is empty ;
hence ex b₁ being ContextStr st
( b₁ is strict & not b₁ is empty ) ; :: thesis: verum