consider A being non empty Subset of the carrier' of C;
consider O being non empty Subset of the carrier of C;
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