let C be FormalContext; for CP being strict FormalConcept of C holds "/\" ( { ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex a being Attribute of C st
( a in the Intent of CP & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) } ,(ConceptLattice C)) = CP
let CP be strict FormalConcept of C; "/\" ( { ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex a being Attribute of C st
( a in the Intent of CP & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) } ,(ConceptLattice C)) = CP
set D = { ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex a being Attribute of C st
( a in the Intent of CP & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) } ;
A1:
for CP9 being Element of (ConceptLattice C) st CP9 is_less_than { ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex a being Attribute of C st
( a in the Intent of CP & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) } holds
CP9 [= @ CP
@ CP is_less_than { ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex a being Attribute of C st
( a in the Intent of CP & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) }
proof
let q be
Element of
(ConceptLattice C);
LATTICE3:def 16 ( not q in { ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex a being Attribute of C st
( a in the Intent of CP & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) } or @ CP [= q )
assume
q in { ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex a being Attribute of C st
( a in the Intent of CP & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) }
;
@ CP [= q
then consider O being
Subset of the
carrier of
C,
A being
Subset of the
carrier' of
C such that A7:
q = ConceptStr(#
O,
A #)
and A8:
ex
a being
Attribute of
C st
(
a in the
Intent of
CP &
O = (AttributeDerivation C) . {a} &
A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) )
;
consider a being
Attribute of
C such that A9:
a in the
Intent of
CP
and A10:
O = (AttributeDerivation C) . {a}
and
A = (ObjectDerivation C) . ((AttributeDerivation C) . {a})
by A8;
A11:
{a} c= the
Intent of
CP
by A9, ZFMISC_1:31;
(
(AttributeDerivation C) . the
Intent of
CP = the
Extent of
CP & the
Extent of
(q @) = (AttributeDerivation C) . {a} )
by A7, A10, CONLAT_1:def 10, CONLAT_1:def 21;
then
the
Extent of
CP c= the
Extent of
(q @)
by A11, CONLAT_1:4;
then A12:
CP is-SubConcept-of q @
by CONLAT_1:def 16;
CP = (@ CP) @
by CONLAT_1:def 21;
hence
@ CP [= q
by A12, CONLAT_1:43;
verum
end;
hence
"/\" ( { ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex a being Attribute of C st
( a in the Intent of CP & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) } ,(ConceptLattice C)) = CP
by A1, LATTICE3:34; verum