set M9 = { ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ( not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E ) } ;
not { ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ( not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E ) } is empty

proof

set CP = the FormalConcept of C;
consider O being Subset of the carrier of C such that
A1: O = the Extent of the FormalConcept of C ;
consider A being Subset of the carrier' of C such that
A2: A = the Intent of the FormalConcept of C ;
A3: (AttributeDerivation C) . A = O by A1, A2, Def9;
A4: (ObjectDerivation C) . O = A by A1, A2, Def9;
then not ConceptStr(# O,A #) is empty by Lm1;
then ConceptStr(# O,A #) in { ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ( not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E ) } by A4, A3;
hence not { ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ( not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E ) } is empty ; :: thesis: verum

end;

then reconsider M9 = { ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ( not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E ) } as non empty set ;
for CP being strict non empty ConceptStr over C holds
( CP in M9 iff ( (ObjectDerivation C) . the Extent of CP = the Intent of CP & (AttributeDerivation C) . the Intent of CP = the Extent of CP ) )

proof

let CP be strict non empty ConceptStr over C; :: thesis: ( CP in M9 iff ( (ObjectDerivation C) . the Extent of CP = the Intent of CP & (AttributeDerivation C) . the Intent of CP = the Extent of CP ) )

now :: thesis: ( CP in M9 implies ( (ObjectDerivation C) . the Extent of CP = the Intent of CP & (AttributeDerivation C) . the Intent of CP = the Extent of CP ) )

assume CP in M9 ; :: thesis: ( (ObjectDerivation C) . the Extent of CP = the Intent of CP & (AttributeDerivation C) . the Intent of CP = the Extent of CP )
then ex E being Subset of the carrier of C ex I being Subset of the carrier' of C st
( CP = ConceptStr(# E,I #) & not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E ) ;
hence ( (ObjectDerivation C) . the Extent of CP = the Intent of CP & (AttributeDerivation C) . the Intent of CP = the Extent of CP ) ; :: thesis: verum

end;

hence ( CP in M9 iff ( (ObjectDerivation C) . the Extent of CP = the Intent of CP & (AttributeDerivation C) . the Intent of CP = the Extent of CP ) ) ; :: thesis: verum

end;

hence { ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ( not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E ) } is non empty set ; :: thesis: verum