consider A being non empty Subset of ;
consider O being non empty Subset of ;
not ConceptStr(# O,A #) is empty by Def11;
hence ex b₁ being ConceptStr of C st
( b₁ is strict & not b₁ is empty ) ; :: thesis: verum