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