let C be FormalContext; :: thesis: 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; :: thesis: "/\" ( { 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

proof

let CP9 be Element of (ConceptLattice C); :: thesis: ( 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}) ) } implies CP9 [= @ CP )
assume A2: 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}) ) } ; :: thesis: CP9 [= @ CP
A3: the Intent of CP c= the Intent of (CP9 @)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the Intent of CP or x in the Intent of (CP9 @) )
assume A4: x in the Intent of CP ; :: thesis: x in the Intent of (CP9 @)
then reconsider x = x as Element of the carrier' of C ;
set Ax = (ObjectDerivation C) . ((AttributeDerivation C) . {x});
set Ox = (AttributeDerivation C) . {x};
reconsider Cx = ConceptStr(# ((AttributeDerivation C) . {x}),((ObjectDerivation C) . ((AttributeDerivation C) . {x})) #) as strict FormalConcept of C by CONLAT_1:21;
Cx 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}) ) } by A4;
then CP9 [= @ Cx by A2;
then A5: CP9 @ is-SubConcept-of (@ Cx) @ by CONLAT_1:43;
{x} c= (ObjectDerivation C) . ((AttributeDerivation C) . {x}) by CONLAT_1:6;
then A6: x in the Intent of Cx by ZFMISC_1:31;
Cx = (@ Cx) @ by CONLAT_1:def 21;
then the Intent of Cx c= the Intent of (CP9 @) by A5, CONLAT_1:28;
hence x in the Intent of (CP9 @) by A6; :: thesis: verum

end;

CP = (@ CP) @ by CONLAT_1:def 21;
then CP9 @ is-SubConcept-of (@ CP) @ by A3, CONLAT_1:28;
hence CP9 [= @ CP by CONLAT_1:43; :: thesis: verum

end;

@ 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); :: according to LATTICE3:def 16 :: thesis: ( 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}) ) } ; :: thesis: @ 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; :: thesis: 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; :: thesis: verum