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
;
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 ) )
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
; verum