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