set A = the non empty Subset of the carrier' of C;
set O = the non empty Subset of the carrier of C;
not ConceptStr(# the non empty Subset of the carrier of C, the non empty Subset of the carrier' of C #) is empty ;
hence ex b₁ being ConceptStr over C st
( b₁ is strict & not b₁ is empty ) ; :: thesis: verum