reconsider A = {} as Subset of the carrier' of C by XBOOLE_1:2;
reconsider O = {} as Subset of the carrier of C by XBOOLE_1:2;
ConceptStr(# O,A #) is quasi-empty ;
hence ex b₁ being ConceptStr over C st
( b₁ is strict & b₁ is quasi-empty ) ; :: thesis: verum